Core definitions for ZFC set theory

This file develops basic definitions and lemmas over ZFSet, including transitive and inductive sets, the symmetric difference, and assorted membership and monotonicity results.

@[simp]

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

theorem ZFSet.insert_def {x y : ZFSet.{u_1}} : insert x y = {x} ∪ y

def ZFSet.transitive (x : ZFSet.{u_1}) : Prop

A set x is transitive if every element of x is a subset of x: ∀ y ∈ x, y ⊆ x.

Equations

• x.transitive = ∀ y ∈ x, y ⊆ x

def ZFSet.termω : Lean.ParserDescr

Equations

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

def ZFSet.inductive_set (E : ZFSet.{u_1}) : Prop

An inductive set is defined as a set that contains the empty set ∅ and is closed under successor.

The "successor" of a set x is defined as the insertion of x into itself.

Equations

• E.inductive_set = (∅ ∈ E ∧ ∀ n ∈ E, insert n n ∈ E)

theorem ZFSet.prod_nonempty {x y : ZFSet.{u_1}} : x ≠ ∅ → y ≠ ∅ → x.prod y ≠ ∅

theorem ZFSet.trans_imp_insert_trans {x : ZFSet.{u_1}} : x.transitive → (insert x x).transitive

theorem ZFSet.inductive_sep {S : ZFSet.{u_1}} (P : ZFSet.{u_1} → Prop) (ind : S.inductive_set) (h₀ : P ∅) (h₁ : ∀ n ∈ S, P n → P (insert n n)) : (ZFSet.sep P S).inductive_set

theorem ZFSet.inductive_imp_transitive {E : ZFSet.{u_1}} : E.inductive_set → (ZFSet.sep transitive E).inductive_set

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

theorem ZFSet.omega_inductive : ω.inductive_set

The first Von Neumann ordinal ω is an inductive set.

def ZFSet.symmDiff (p q : ZFSet.{u_1}) : ZFSet.{u_1}

Equations

• p Δ q = p \ q ∪ q \ p

def ZFSet.term_Δ_ : Lean.TrailingParserDescr

Equations

• ZFSet.term_Δ_ = Lean.ParserDescr.trailingNode `ZFSet.term_Δ_ 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " Δ ") (Lean.ParserDescr.cat `term 71))

@[simp]

theorem ZFSet.mem_symmDiff (x p q : ZFSet.{u_1}) : x ∈ p Δ q ↔ x ∈ p ∧ x ∉ q ∨ x ∈ q ∧ x ∉ p

@[simp]

theorem ZFSet.symmDiff_empty (p : ZFSet.{u_1}) : p Δ ∅ = p

theorem ZFSet.symmDiff_comm (p q : ZFSet.{u_1}) : p Δ q = q Δ p

@[simp]

theorem ZFSet.symmDiff_self (p : ZFSet.{u_1}) : p Δ p = ∅

@[implicit_reducible]

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

Equations

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

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.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