Basic ZFSet lemmas

This file develops elementary lemmas about ZFSet, including characterizations of the empty set, separation, and the behavior of unions and intersections.

theorem ZFSet.nonempty_exists_iff {n : ZFSet.{u_1}} : n ≠ ∅ ↔ ∃ (m : ZFSet.{u_1}), m ∈ n

theorem ZFSet.subset_of_empty {x : ZFSet.{u_1}} (h : x ⊆ ∅) : x = ∅

theorem ZFSet.sep_subset_self {P : ZFSet.{u_1} → Prop} {a : ZFSet.{u_1}} : ZFSet.sep P a ⊆ a

theorem ZFSet.sUnion_insert {x : ZFSet.{u_1}} : (insert x x).sUnion = x ∪ x.sUnion

theorem ZFSet.singleton_subset_mem_iff {x y : ZFSet.{u_1}} : {x} ⊆ y ↔ x ∈ y

theorem ZFSet.sInter_pair {a b : ZFSet.{u_1}} : {a, b}.sInter = a ∩ b

@[simp]

theorem ZFSet.sep_empty_iff {A : ZFSet.{u_1}} {P : ZFSet.{u_1} → Prop} : ZFSet.sep P A = ∅ ↔ A = ∅ ∨ ∀ x ∈ A, ¬P x

theorem ZFSet.insert_prod {A B x : ZFSet.{u_1}} : (insert x A).prod B = A.prod B ∪ {x}.prod B

theorem ZFSet.prod_insert {A B x : ZFSet.{u_1}} : A.prod (insert x B) = A.prod B ∪ A.prod {x}

theorem ZFSet.union_empty {A : ZFSet.{u_1}} : A ∪ ∅ = A

theorem ZFSet.inter_comm {A B : ZFSet.{u_1}} : A ∩ B = B ∩ A

theorem ZFSet.union_comm {A B : ZFSet.{u_1}} : A ∪ B = B ∪ A

theorem ZFSet.empty_union {A : ZFSet.{u_1}} : ∅ ∪ A = A

@[simp]

theorem ZFSet.mem_powerset_self {x : ZFSet.{u_1}} : x ∈ x.powerset

theorem ZFSet.inter_self {A : ZFSet.{u_1}} : A ∩ A = A

theorem ZFSet.inter_empty {A : ZFSet.{u_1}} : A ∩ ∅ = ∅

theorem ZFSet.empty_inter {A : ZFSet.{u_1}} : ∅ ∩ A = ∅

theorem ZFSet.union_self {A : ZFSet.{u_1}} : A ∪ A = A

theorem ZFSet.sep_true {A : ZFSet.{u_1}} : ZFSet.sep (fun (x : ZFSet.{u_1}) => True) A = A

theorem ZFSet.powerset_mono {x y : ZFSet.{u_1}} : x ⊆ y → x.powerset ⊆ y.powerset

@[simp]

theorem ZFSet.prod_empty_right {x : ZFSet.{u_1}} : x.prod ∅ = ∅

@[simp]

theorem ZFSet.prod_empty_left {x : ZFSet.{u_1}} : ∅.prod x = ∅

def ZFSet.termε : Lean.ParserDescr

Equations

• ZFSet.termε = Lean.ParserDescr.node `ZFSet.termε 1024 (Lean.ParserDescr.symbol " ε ")

theorem ZFSet.eq_of_subset_subset {A B : ZFSet.{u_1}} (hAB : A ⊆ B) (hBA : B ⊆ A) : A = B

theorem ZFSet.powerset_inj {A B : ZFSet.{u_1}} (h : A.powerset = B.powerset) : A = B

theorem ZFSet.prod_inj {A B C D : ZFSet.{u_1}} (h : A.prod B = C.prod D) (hA : A ≠ ∅) (hB : B ≠ ∅) : A = C ∧ B = D