LeanPool.ZFLean.Basic

Imported Lean Pool material for LeanPool.ZFLean.Basic.

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

@[simp]

theorem ZFSet.not_nonempty_is_empty {x : ZFSet.{u_1}} : ¬x.Nonempty ↔ x = ∅

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.insert_def {x y : ZFSet.{u_1}} : insert 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.prod_nonempty {x y : ZFSet.{u_1}} : x ≠ ∅ → y ≠ ∅ → x.prod y ≠ ∅

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

theorem ZFSet.union_mono {x y z : ZFSet.{u_1}} : x ⊆ z → y ⊆ z → x ∪ y ⊆ z

theorem ZFSet.inter_mono {x y z : ZFSet.{u_1}} : x ⊆ z → y ⊆ z → x ∩ y ⊆ z

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 = ∅

@[implicit_reducible]

instance ZFSet.ZFSetSProdinst : SProd ZFSet.{u_1} ZFSet.{u_1} ZFSet.{u_1}

Equations

• ZFSet.ZFSetSProdinst = { sprod := ZFSet.prod }

def ZFSet.termε : Lean.ParserDescr

Imported ZFLean declaration.

Equations

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

theorem ZFSet.epsilon_mem {y : ZFSet.{u_1}} (hy : y ≠ ∅) : (fun (x : ZFSet.{u_1}) => Classical.epsilon fun (z : ZFSet.{u_1}) => z ∈ x) y ∈ y

theorem ZFSet.insert_mem {x y : ZFSet.{u_1}} (h : x ∈ y) : insert x y = y

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