Functions and relations on ZF sets

This file develops binary relations, partial and total functions, composition, identity, injectivity/surjectivity/bijectivity, permutations, lambda abstraction and function application on the encoded ZFSet universe, together with order-theoretic notions on subsets.

def ZFSet.inv (R : ZFSet.{u_1}) {A B : ZFSet.{u_1}} (isRel : R ⊆ A.prod B := by zrel) : ZFSet.{u_1}

Inverse of a (binary) relation. A proof that R is a relation is needed and tried to be automatically inferred.

Equations

• R⁻¹ isRel = ZFSet.sep (fun (yx : ZFSet.{?u.1}) => have x := yx.π₂; have y := yx.π₁; x.pair y ∈ R) (B.prod A)

def ZFSet.«term_⁻¹» : Lean.TrailingParserDescr

Equations

• ZFSet.«term_⁻¹» = Lean.ParserDescr.trailingNode `ZFSet.«term_⁻¹» 1024 1024 (Lean.ParserDescr.symbol "⁻¹")

theorem ZFSet.mem_inv {x y R A B : ZFSet.{u_1}} (hR : R ⊆ A.prod B) : y.pair x ∈ R⁻¹ hR ↔ x.pair y ∈ R

theorem ZFSet.subset_prod_inv {R A B : ZFSet.{u_1}} (hR : R ⊆ A.prod B) : R⁻¹ hR ⊆ B.prod A

theorem ZFSet.inv_involutive {R A B : ZFSet.{u_1}} (hR : R ⊆ A.prod B) : (R⁻¹ hR)⁻¹ ⋯ = R

@[reducible, inline]

abbrev ZFSet.Dom (f : ZFSet.{u_1}) {A B : ZFSet.{u_1}} (hf : f ⊆ A.prod B := by zrel) : ZFSet.{u_1}

Domain of a (binary) relation. A proof that f is a relation is needed and tried to be automatically inferred.

Equations

• f.Dom hf = ZFSet.sep (fun (x : ZFSet.{?u.1}) => ∃ y ∈ B, x.pair y ∈ f) A

@[reducible, inline]

abbrev ZFSet.Range (f : ZFSet.{u_1}) {A B : ZFSet.{u_1}} (hf : f ⊆ A.prod B := by zrel) : ZFSet.{u_1}

Equations

• f.Range hf = ZFSet.sep (fun (y : ZFSet.{?u.1}) => ∃ x ∈ f.Dom hf, x.pair y ∈ f) B

theorem ZFSet.funs.nonempty {A B : ZFSet.{u_1}} (hB : B ≠ ∅) : A.funs B ≠ ∅

def ZFSet.IsPFunc (f A B : ZFSet.{u_1}) : Prop

IsPFunc f A B is the assertion that f is a partial function from A to B, i.e. that if pair x y ∈ f and pair x z ∈ f then y = z.

Equations

• f.IsPFunc A B = (f ⊆ A.prod B ∧ ∀ (x y : ZFSet.{?u.1}), x.pair y ∈ f → ∀ (z : ZFSet.{?u.1}), x.pair z ∈ f → y = z)

theorem ZFSet.is_rel_of_is_pfunc {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) : f ⊆ A.prod B

theorem ZFSet.pfunc_weaken {f A B C D : ZFSet.{u_1}} (hf : f.IsPFunc C D) (hAB : C ⊆ A) (hCD : D ⊆ B) : f.IsPFunc A B

theorem ZFSet.is_func_is_pfunc {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) : f.IsPFunc A B

theorem ZFSet.is_rel_of_is_func {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) : f ⊆ A.prod B

theorem ZFSet.is_func_extend_range {f D E : ZFSet.{u_1}} (hf : D.IsFunc E f) {F : ZFSet.{u_1}} (sub_E_F : E ⊆ F) : D.IsFunc F f

@[simp]

theorem ZFSet.is_func_empty : ∅.IsFunc ∅ ∅

theorem ZFSet.is_pfunc_func_exists {f A B : ZFSet.{u_1}} : f.IsPFunc A B → ∃ (A' : ZFSet.{u_1}) (B' : ZFSet.{u_1}), A'.IsFunc B' f ∧ A' ⊆ A ∧ B' ⊆ B

theorem ZFSet.pfun_dom_subset (f : ZFSet.{u_1}) {A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) : f.Dom ⋯ ⊆ A

theorem ZFSet.mem_dom {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) {x y : ZFSet.{u_1}} : x.pair y ∈ f → x ∈ f.Dom ⋯

theorem ZFSet.is_func_dom_range (f : ZFSet.{u_1}) {A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) : (f.Dom ⋯).IsFunc (f.Range ⋯) f

theorem ZFSet.is_func_of_pfunc (f : ZFSet.{u_1}) {A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) : (f.Dom ⋯).IsFunc B f

def ZFSet.IsInjective (f : ZFSet.{u_1}) {A B : ZFSet.{u_1}} (hf : A.IsFunc B f := by zfun) : Prop

Equations

• f.IsInjective hf = ∀ (x y z : ZFSet.{?u.1}), x ∈ A → y ∈ A → z ∈ B → x.pair z ∈ f → y.pair z ∈ f → x = y

def ZFSet.IsSurjective (f : ZFSet.{u_1}) {A B : ZFSet.{u_1}} (hf : A.IsFunc B f := by zfun) : Prop

Equations

• f.IsSurjective hf = ∀ y ∈ B, ∃ x ∈ A, x.pair y ∈ f

def ZFSet.IsBijective (f : ZFSet.{u_1}) {A B : ZFSet.{u_1}} (hf : A.IsFunc B f := by zfun) : Prop

Equations

• f.IsBijective hf = (f.IsInjective hf ∧ f.IsSurjective hf)

theorem ZFSet.IsInjective.ofBijective {f A B C : ZFSet.{u_1}} {hf : A.IsFunc B f} (f_bij : f.IsBijective hf) (B_sub_C : B ⊆ C) : f.IsInjective ⋯

theorem ZFSet.bijective_exists1_iff {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) : f.IsBijective hf ↔ ∀ y ∈ B, ∃! x : ZFSet.{u_1}, x ∈ A ∧ x.pair y ∈ f

def ZFSet.IsMono {f A B : ZFSet.{u_1}} [LTA : Preorder ↥A] [LTB : Preorder ↥B] : A.IsFunc B f → Prop

Equations

• One or more equations did not get rendered due to their size.

def ZFSet.IsStrictMono {f A B : ZFSet.{u_1}} [LTA : Preorder ↥A] [LTB : Preorder ↥B] : A.IsFunc B f → Prop

Equations

• One or more equations did not get rendered due to their size.

def ZFSet.Id (A : ZFSet.{u_1}) : ZFSet.{u_1}

Equations

• 𝟙A = ZFSet.sep (fun (x : ZFSet.{?u.1}) => ∃ y ∈ A, x = y.pair y) (A.prod A)

def ZFSet.«term𝟙_» : Lean.ParserDescr

Equations

• ZFSet.«term𝟙_» = Lean.ParserDescr.node `ZFSet.«term𝟙_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝟙") (Lean.ParserDescr.cat `term 1024))

theorem ZFSet.pair_mem_Id_iff {A x y : ZFSet.{u_1}} (hx : x ∈ A) : x.pair y ∈ 𝟙A ↔ x = y

theorem ZFSet.mem_Id_iff {A z : ZFSet.{u_1}} : z ∈ 𝟙A ↔ ∃ x ∈ A, z = x.pair x

theorem ZFSet.pair_self_mem_Id {A x : ZFSet.{u_1}} (hx : x ∈ A) : x.pair x ∈ 𝟙A

theorem ZFSet.Id.IsFunc {A : ZFSet.{u_1}} : A.IsFunc A 𝟙A

theorem ZFSet.Id.IsPFunc {A : ZFSet.{u_1}} : (𝟙A).IsPFunc A A

theorem ZFSet.Id.IsBijective {A : ZFSet.{u_1}} : (𝟙A).IsBijective ⋯

@[simp]

theorem ZFSet.range_Id {A : ZFSet.{u_1}} : (𝟙A).Range ⋯ = A

def ZFSet.IsPermutation (σ E : ZFSet.{u_1}) : Prop

Equations

• σ.IsPermutation E = ∃ (hσ : E.IsFunc E σ), σ.IsBijective hσ

def ZFSet.permutations (E : ZFSet.{u_1}) : ZFSet.{u_1}

Equations

• E.permutations = ZFSet.sep (fun (f : ZFSet.{?u.1}) => f.IsPermutation E) (E.funs E)

theorem ZFSet.Id.IsPermutation {A : ZFSet.{u_1}} : (𝟙A).IsPermutation A

def ZFSet.composition (g f A B C : ZFSet.{u_1}) : ZFSet.{u_1}

If f : A → B and g : B → C are functions, then composition g f is the function from A to C defined by composition g f (x, z) = (x, y) where y is such that (x, y) ∈ f and (y, z) ∈ g.

Equations

• g.composition f A B C = ZFSet.sep (fun (xz : ZFSet.{?u.1}) => ∃ (x : ZFSet.{?u.1}) (z : ZFSet.{?u.1}), xz = x.pair z ∧ ∃ y ∈ B, x.pair y ∈ f ∧ y.pair z ∈ g) (A.prod C)

theorem ZFSet.mem_composition (g f : ZFSet.{u_1}) {A B C z : ZFSet.{u_1}} : z ∈ g.composition f A B C ↔ ∃ (x : ZFSet.{u_1}) (w : ZFSet.{u_1}) (y : ZFSet.{u_1}), z = x.pair y ∧ x ∈ A ∧ y ∈ C ∧ w ∈ B ∧ x.pair w ∈ f ∧ w.pair y ∈ g

theorem ZFSet.Id.composition_left {f A B : ZFSet.{u_1}} (hf : f ⊆ A.prod B) : (𝟙B).composition f A B B = f

theorem ZFSet.Id.composition_right {f A B : ZFSet.{u_1}} (hf : f ⊆ A.prod B) : f.composition (𝟙A) A A B = f

theorem ZFSet.IsPFunc_of_composition_IsPFunc {f g A B C : ZFSet.{u_1}} (hf : f.IsPFunc A B) (hg : g.IsPFunc B C) : (g.composition f A B C).IsPFunc A C

theorem ZFSet.IsFunc_of_composition_IsFunc {g f A B C : ZFSet.{u_1}} (hg : B.IsFunc C g) (hf : A.IsFunc B f) : A.IsFunc C (g.composition f A B C)

@[reducible, inline]

abbrev ZFSet.fcomp (g f : ZFSet.{u_1}) {A B C : ZFSet.{u_1}} (hg : B.IsFunc C g := by zfun) (hf : A.IsFunc B f := by zfun) : ZFSet.{u_1}

Equations

• (g ∘ᶻ f) hg hf = g.composition f A B C

def ZFSet.«term_∘ᶻ_» : Lean.TrailingParserDescr

Equations

• ZFSet.«term_∘ᶻ_» = Lean.ParserDescr.trailingNode `ZFSet.«term_∘ᶻ_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ᶻ ") (Lean.ParserDescr.cat `term 91))

@[simp]

theorem ZFSet.pair_mem_composition (g f : ZFSet.{u_1}) {A B C x y : ZFSet.{u_1}} (hg : B.IsFunc C g) (hf : A.IsFunc B f) : x.pair y ∈ (g ∘ᶻ f) hg hf ↔ ∃ w ∈ B, x.pair w ∈ f ∧ w.pair y ∈ g

theorem ZFSet.IsInjective.composition_of_injective {f g A B C : ZFSet.{u_1}} {hf : A.IsFunc B f} {hg : B.IsFunc C g} (finj : f.IsInjective hf) (ginj : g.IsInjective hg) : ((g ∘ᶻ f) hg hf).IsInjective ⋯

theorem ZFSet.IsSurjective.composition_of_surjective {f g A B C : ZFSet.{u_1}} {hf : A.IsFunc B f} {hg : B.IsFunc C g} (fsurj : f.IsSurjective hf) (gsurj : g.IsSurjective hg) : ((g ∘ᶻ f) hg hf).IsSurjective ⋯

theorem ZFSet.IsBijective.composition_of_bijective {f g A B C : ZFSet.{u_1}} {hf : A.IsFunc B f} {hg : B.IsFunc C g} (fbij : f.IsBijective hf) (gbij : g.IsBijective hg) : ((g ∘ᶻ f) hg hf).IsBijective ⋯

theorem ZFSet.IsPermutation.composition_of_permutations {σ τ E : ZFSet.{u_1}} (hσ : σ.IsPermutation E) (hτ : τ.IsPermutation E) : (τ.composition σ E E E).IsPermutation E

@[simp]

theorem ZFSet.composition_assoc {A B C D f g h : ZFSet.{u_1}} : h.composition (g.composition f A B C) A C D = (h.composition g B C D).composition f A B D

@[simp]

theorem ZFSet.fcomp_assoc {A B C D f g h : ZFSet.{u_1}} (hf : A.IsFunc B f) (hg : B.IsFunc C g) (hh : C.IsFunc D h) : (h ∘ᶻ (g ∘ᶻ f) hg hf) hh ⋯ = ((h ∘ᶻ g) hh hg ∘ᶻ f) ⋯ hf

noncomputable def ZFSet.fapply (f : ZFSet.{u_1}) {A B : ZFSet.{u_1}} (hf : f.IsPFunc A B := by zpfun) : ↥(f.Dom ⋯) → ↥B

Equations

• @ᶻf hf ⟨x_1, x_dom⟩ = ⟨Classical.choose ⋯, ⋯⟩

def ZFSet.«term@ᶻ_» : Lean.ParserDescr

Equations

• ZFSet.«term@ᶻ_» = Lean.ParserDescr.node `ZFSet.«term@ᶻ_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@ᶻ") (Lean.ParserDescr.cat `term 1024))

@[simp]

theorem ZFSet.is_func_dom_eq {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f := by zfun) : f.Dom ⋯ = A

Seed lemmas for the zdom tactic

is_func_dom_eq is an equation, so solve_by_elim — which only ever applys a lemma's conclusion — cannot use it. The following elimination-shaped lemmas are its membership counterparts, and are what makes zdom able to close the side conditions of @ᶻ.

theorem ZFSet.mem_dom_of_mem {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) {x : ZFSet.{u_1}} (hx : x ∈ A) : x ∈ f.Dom ⋯

Membership form of is_func_dom_eq: the domain of a function IsFunc A B f contains every element of A.

theorem ZFSet.mem_of_mem_dom {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) {x : ZFSet.{u_1}} (hx : x ∈ f.Dom ⋯) : x ∈ A

Converse of mem_dom_of_mem: the domain of a partial function is contained in its source. A zdom_conv seed rather than a zdom one: in the main search it would let solve_by_elim loop between x ∈ A and x ∈ f.Dom (see ZFLean/Tactics.lean).

theorem ZFSet.pair_mem_prod_of_mem {A B a b : ZFSet.{u_1}} (ha : a ∈ A) (hb : b ∈ B) : a.pair b ∈ A.prod B

Introduction form of pair_mem_prod.

theorem ZFSet.mem_funs_of_is_func {A B f : ZFSet.{u_1}} (hf : A.IsFunc B f) : f ∈ A.funs B

Introduction form of mem_funs.

theorem ZFSet.mem_powerset_of_subset {A B : ZFSet.{u_1}} (h : A ⊆ B) : A ∈ B.powerset

Introduction form of mem_powerset.

theorem ZFSet.fapply_Id {A x : ZFSet.{u_1}} (hx : x ∈ A) : @ᶻ𝟙A ⋯ ⟨x, ⋯⟩ = ⟨x, hx⟩

theorem ZFSet.fapply_mem_range {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) {x : ZFSet.{u_1}} (hx : x ∈ f.Dom ⋯) : ↑(@ᶻf hf ⟨x, hx⟩) ∈ B

theorem ZFSet.fapply.def {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) {x : ZFSet.{u_1}} (hx : x ∈ f.Dom ⋯) : x.pair ↑(@ᶻf hf ⟨x, hx⟩) ∈ f

theorem ZFSet.IsInjective.apply_inj {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) (inj : f.IsInjective hf) : Function.Injective (@ᶻf ⋯)

theorem ZFSet.IsPFunc.exists_unique_of_mem_dom {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) {x : ZFSet.{u_1}} (hx : x ∈ f.Dom ⋯) : ∃! y : ZFSet.{u_1}, x.pair y ∈ f

theorem ZFSet.fapply.of_pair {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) {x y : ZFSet.{u_1}} (hxy : x.pair y ∈ f) : @ᶻf hf ⟨x, ⋯⟩ = ⟨y, ⋯⟩

theorem ZFSet.IsPFunc.supset_of_range {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) : f.Range ⋯ ⊆ B

theorem ZFSet.IsPFunc.mem_range_of_mem {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) {x y : ZFSet.{u_1}} (hxy : x.pair y ∈ f) : y ∈ f.Range ⋯

theorem ZFSet.IsPFunc.nonempty_range_of_nonempty_dom {f A B x y : ZFSet.{u_1}} (hf : f.IsPFunc A B) (hxy : x.pair y ∈ f) : f.Range ⋯ ≠ ∅

theorem ZFSet.IsInjective.apply_inj_pfun {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) (inj : f.IsInjective ⋯) : Function.Injective (@ᶻf hf)

theorem ZFSet.IsInjective.apply_surj {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) (surj : f.IsSurjective hf) : Function.Surjective (@ᶻf ⋯)

theorem ZFSet.IsInjective.apply_surj_pfun {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) (surj : f.IsSurjective ⋯) : Function.Surjective (@ᶻf hf)

theorem ZFSet.prod_sep_is_pfunc_mem {A B C D : ZFSet.{u_1}} (subAC : A ⊆ C) (subBD : B ⊆ D) : ZFSet.sep (fun (x : ZFSet.{u_1}) => x.IsPFunc A B) (A.prod B).powerset ∈ (C.prod D).powerset.powerset

def ZFSet.lambda (dom ran : ZFSet.{u_1}) (exp : ZFSet.{u_1} → ZFSet.{u_1}) : ZFSet.{u_1}

Equations

• dom.lambda ran exp = ZFSet.sep (fun (xy : ZFSet.{?u.1}) => xy.π₂ = exp xy.π₁) (dom.prod ran)

def ZFSet.funz_binder.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.funz_binder : Category

Equations

• Lean.Parser.Category.funz_binder = { }

def ZFSet.identZBinder : Lean.ParserDescr

Equations

• ZFSet.identZBinder = Lean.ParserDescr.node `ZFSet.identZBinder 1022 (Lean.ParserDescr.parser `Lean.Parser.Term.ident)

def ZFSet.tupleZBinder : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def ZFSet.funZBinder : Lean.Parser.Parser

Equations

• ZFSet.funZBinder = Lean.Parser.categoryParser `funz_binder 0

def ZFSet.funZType : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def ZFSet.funZAlts : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def ZFSet.basicFunZ : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def ZFSet.funZ : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

partial def ZFSet.interpZBinder (x_def e : Lean.TSyntax `term) : Lean.TSyntax `funz_binder → Lean.MacroM (Lean.TSyntax `term)

theorem ZFSet.lambda_spec {dom ran : ZFSet.{u_1}} {exp : ZFSet.{u_1} → ZFSet.{u_1}} {x y : ZFSet.{u_1}} : (x.pair y ∈ dom.lambda ran fun (a : ZFSet.{u_1}) => exp a) ↔ x ∈ dom ∧ y ∈ ran ∧ y = exp x

theorem ZFSet.mem_lambda {dom ran : ZFSet.{u_1}} {exp : ZFSet.{u_1} → ZFSet.{u_1}} {z : ZFSet.{u_1}} : (z ∈ dom.lambda ran fun (a : ZFSet.{u_1}) => exp a) ↔ ∃ (x : ZFSet.{u_1}) (y : ZFSet.{u_1}), z = x.pair y ∧ x ∈ dom ∧ y ∈ ran ∧ y = exp x

theorem ZFSet.lambda_ext_iff {d r : ZFSet.{u_1}} {f₁ f₂ : ZFSet.{u_1} → ZFSet.{u_1}} (hf₁ : ∀ {x : ZFSet.{u_1}}, x ∈ d → f₁ x ∈ r) : ((d.lambda r fun (a : ZFSet.{u_1}) => f₁ a) = d.lambda r fun (a : ZFSet.{u_1}) => f₂ a) ↔ ∀ z ∈ d, f₁ z = f₂ z

theorem ZFSet.lambda_ext_iff' {d₁ d₂ r₁ r₂ : ZFSet.{u_1}} {f₁ f₂ : ZFSet.{u_1} → ZFSet.{u_1}} (hf₁ : ∀ {x : ZFSet.{u_1}}, x ∈ d₁ → f₁ x ∈ r₁) (hf₂ : ∀ {x : ZFSet.{u_1}}, x ∈ d₂ → f₂ x ∈ r₂) : ((d₁.lambda r₁ fun (a : ZFSet.{u_1}) => f₁ a) = d₂.lambda r₂ fun (a : ZFSet.{u_1}) => f₂ a) ↔ d₁ = d₂ ∧ ∀ z ∈ d₁, f₁ z = f₂ z

theorem ZFSet.lambda_eta {A B f : ZFSet.{u_1}} (hf : A.IsFunc B f) : f = A.lambda B fun (a : ZFSet.{u_1}) => if hx : a ∈ A then ↑(@ᶻf ⋯ ⟨a, ⋯⟩) else ∅

theorem ZFSet.is_func_ext_iff {A B f g : ZFSet.{u_1}} (hf : A.IsFunc B f) (hg : A.IsFunc B g) : f = g ↔ ∀ (x : ZFSet.{u_1}) (hx : x ∈ A), @ᶻf ⋯ ⟨x, ⋯⟩ = @ᶻg ⋯ ⟨x, ⋯⟩

theorem ZFSet.lambda_subset {A B : ZFSet.{u_1}} {exp : ZFSet.{u_1} → ZFSet.{u_1}} : A.lambda B exp ⊆ A.prod B

theorem ZFSet.lambda_isFunc {A B : ZFSet.{u_1}} {f : ZFSet.{u_1} → ZFSet.{u_1}} (hf : ∀ {x : ZFSet.{u_1}}, x ∈ A → f x ∈ B) : A.IsFunc B (A.lambda B f)

theorem ZFSet.mem_funs_of_lambda {A B : ZFSet.{u_1}} {f : ZFSet.{u_1} → ZFSet.{u_1}} (hf : ∀ {x : ZFSet.{u_1}}, x ∈ A → f x ∈ B) : A.lambda B f ∈ A.funs B

theorem ZFSet.fapply_lambda {A B : ZFSet.{u_1}} {f : ZFSet.{u_1} → ZFSet.{u_1}} (hf : ∀ {x : ZFSet.{u_1}}, x ∈ A → f x ∈ B) {a : ZFSet.{u_1}} (ha : a ∈ A) : ↑(@ᶻ(A.lambda B fun (a : ZFSet.{u_1}) => f a) ⋯ ⟨a, ⋯⟩) = f a

theorem ZFSet.inv_is_func_of_injective {f A B : ZFSet.{u_1}} {f_is_func : A.IsFunc B f} (hf : f.IsInjective f_is_func) : (f.Range ⋯).IsFunc A (f⁻¹ ⋯)

The inverse of an injection is a function.

theorem ZFSet.inv_is_func_of_bijective {f A B : ZFSet.{u_1}} {f_is_func : A.IsFunc B f} (hf : f.IsBijective f_is_func) : B.IsFunc A (f⁻¹ ⋯)

The inverse of a bijection is a function.

theorem ZFSet.inv_bijective_of_bijective {f A B : ZFSet.{u_1}} {f_is_func : A.IsFunc B f} (hf : f.IsBijective f_is_func) : (f⁻¹ ⋯).IsBijective ⋯

The inverse of a bijection is a bijection.

theorem ZFSet.composition_self_inv_of_bijective {f A B : ZFSet.{u_1}} {f_is_func : A.IsFunc B f} (hf : f.IsBijective f_is_func) : (f⁻¹ ⋯ ∘ᶻ f) ⋯ f_is_func = 𝟙A

theorem ZFSet.composition_inv_self_of_bijective {f A B : ZFSet.{u_1}} {f_is_func : A.IsFunc B f} (hf : f.IsBijective f_is_func) : (f ∘ᶻ f⁻¹ ⋯) f_is_func ⋯ = 𝟙B

theorem ZFSet.inv_fcomp_iff {A B C f g : ZFSet.{u_1}} {hf : A.IsFunc B f} (fbij : f.IsBijective hf) {hg : B.IsFunc C g} (gbij : g.IsBijective hg) : ((g ∘ᶻ f) hg hf)⁻¹ ⋯ = (f⁻¹ ⋯ ∘ᶻ g⁻¹ ⋯) ⋯ ⋯

theorem ZFSet.fcomp_bij_fcomp_inv_right {A B C f g h : ZFSet.{u_1}} {hf : A.IsFunc B f} (hbij : f.IsBijective hf) (hg : B.IsFunc C g) (hh : A.IsFunc C h) : (g ∘ᶻ f) hg hf = h ↔ g = (h ∘ᶻ f⁻¹ ⋯) hh ⋯

theorem ZFSet.fcomp_bij_fcomp_inv_left {A B C f g h : ZFSet.{u_1}} {hf : B.IsFunc C f} (hbij : f.IsBijective hf) (hg : A.IsFunc B g) (hh : A.IsFunc C h) : (f ∘ᶻ g) hf hg = h ↔ g = (f⁻¹ ⋯ ∘ᶻ h) ⋯ hh

@[simp]

theorem ZFSet.fcomp_bij_right_cancel_iff {A B C f : ZFSet.{u_1}} {hf : A.IsFunc B f} (hbij : f.IsBijective hf) {g₁ g₂ : ZFSet.{u_1}} (hg₁ : B.IsFunc C g₁) (hg₂ : B.IsFunc C g₂) : (g₁ ∘ᶻ f) hg₁ hf = (g₂ ∘ᶻ f) hg₂ hf ↔ g₁ = g₂

@[simp]

theorem ZFSet.fcomp_bij_left_cancel_iff {A B C f : ZFSet.{u_1}} {hf : B.IsFunc C f} (hbij : f.IsBijective hf) {g₁ g₂ : ZFSet.{u_1}} (hg₁ : A.IsFunc B g₁) (hg₂ : A.IsFunc B g₂) : (f ∘ᶻ g₁) hf hg₁ = (f ∘ᶻ g₂) hf hg₂ ↔ g₁ = g₂

def ZFSet.Image (R : ZFSet.{u_1}) {A B : ZFSet.{u_1}} (X : ZFSet.{u_1}) (hR : R ⊆ A.prod B := by zrel) : ZFSet.{u_1}

The image of a set under a relation.

Equations

• (R[X]) hR = ZFSet.sep (fun (y : ZFSet.{?u.1}) => ∃ x ∈ X, x.pair y ∈ R) B

def ZFSet.«term_[_]» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem ZFSet.mem_Image {R A B X y : ZFSet.{u_1}} (hR : R ⊆ A.prod B) : y ∈ (R[X]) hR ↔ y ∈ B ∧ ∃ x ∈ X, x.pair y ∈ R

@[simp]

theorem ZFSet.Image_empty {R A B : ZFSet.{u_1}} (hR : R ⊆ A.prod B) : (R[∅]) hR = ∅

theorem ZFSet.Image_of_singleton_pair_mem_iff {A B f : ZFSet.{u_1}} (hf : A.IsFunc B f) {a b : ZFSet.{u_1}} : a.pair b ∈ f ↔ (f[{a}]) ⋯ = {b}

theorem ZFSet.eq_singleton_of_bijective_inv_Image_of_singleton {A B f : ZFSet.{u_1}} {hf : A.IsFunc B f} (hbij : f.IsBijective hf) {b : ZFSet.{u_1}} (hb : b ∈ B) : ∃ a ∈ A, ((f⁻¹ ⋯)[{b}]) ⋯ = {a}

theorem ZFSet.Image_singleton_eq_fapply {A B f : ZFSet.{u_1}} (hf : A.IsFunc B f) {a : ZFSet.{u_1}} (ha : a ∈ A) : (f[{a}]) ⋯ = {↑(@ᶻf ⋯ ⟨a, ⋯⟩)}

theorem ZFSet.fapply_eq_Image_singleton {A B f : ZFSet.{u_1}} (hf : A.IsFunc B f) {a : ZFSet.{u_1}} (ha : a ∈ A) : ↑(@ᶻf ⋯ ⟨a, ⋯⟩) = ((f[{a}]) ⋯).sInter

theorem ZFSet.fapply_composition {g f A B C : ZFSet.{u_1}} (hg : B.IsFunc C g) (hf : A.IsFunc B f) {x : ZFSet.{u_1}} (xA : x ∈ A) : @ᶻ((g ∘ᶻ f) hg hf) ⋯ ⟨x, ⋯⟩ = @ᶻg ⋯ ⟨↑(@ᶻf ⋯ ⟨x, ⋯⟩), ⋯⟩

@[simp]

theorem ZFSet.Image_of_composition_inv_self_of_bijective {f A B : ZFSet.{u_1}} {f_is_func : A.IsFunc B f} (hf : f.IsBijective f_is_func) {X : ZFSet.{u_1}} (hX : X ⊆ A) : ((f⁻¹ ⋯)[(f[X]) ⋯]) ⋯ = X

@[simp]

theorem ZFSet.Image_of_composition_self_inv_of_bijective {f A B : ZFSet.{u_1}} {f_is_func : A.IsFunc B f} (hf : f.IsBijective f_is_func) {X : ZFSet.{u_1}} (hX : X ⊆ B) : (f[((f⁻¹ ⋯)[X]) ⋯]) ⋯ = X

theorem ZFSet.fapply_inv_of_bijective {A B f : ZFSet.{u_1}} {hf : A.IsFunc B f} (f_bij : f.IsBijective hf) {x y : ZFSet.{u_1}} (hx : x ∈ A) (hy : y ∈ B) : ↑(@ᶻf ⋯ ⟨x, ⋯⟩) = y → ↑(@ᶻ(f⁻¹ ⋯) ⋯ ⟨y, ⋯⟩) = x

theorem ZFSet.fapply_inv_of_bijective_iff {A B f : ZFSet.{u_1}} {hf : A.IsFunc B f} (f_bij : f.IsBijective hf) {x y : ZFSet.{u_1}} (hx : x ∈ A) (hy : y ∈ B) : ↑(@ᶻf ⋯ ⟨x, ⋯⟩) = y ↔ ↑(@ᶻ(f⁻¹ ⋯) ⋯ ⟨y, ⋯⟩) = x

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

A set is finite if it is equinumerous to a (ZF) natural number, i.e. if there is a bijection between the set and a natural number.

Equations

• x.IsFinite = ∃ (n : ZFSet.{?u.1}) (f : ZFSet.{?u.1}) (_ : n ∈ ZFSet.Nat) (hf : f ∈ x.funs n), f.IsInjective ⋯

@[reducible, inline]

abbrev ZFSet.ZFFinSet : Type (u_1 + 1)

Equations

• ZFSet.ZFFinSet = { x : ZFSet.{?u.1} // x.IsFinite }

noncomputable def ZFSet.Max (S : ZFSet.{u_1}) [linord : LinearOrder ↥S] : ZFSet.{u_1}

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ZFSet.Min (S : ZFSet.{u_1}) [linord : LinearOrder ↥S] : ZFSet.{u_1}

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def ZFSet.LinearOrder.ofSubset {S T : ZFSet.{u_1}} (S_T : S ⊆ T) [linordT : LinearOrder ↥T] : LinearOrder ↥S

Equations

• ZFSet.LinearOrder.ofSubset S_T = LinearOrder.lift' (fun (x : ↥S) => match x with | ⟨x, hx⟩ => ⟨x, ⋯⟩) ⋯

theorem ZFSet.Min_exists {S : ZFFinSet} [linord : LinearOrder ↥↑S] (nempS : (↑S).Nonempty) : ∃ (x : ↥↑S), ∀ (y : ZFSet.{u_1}) (y_S : y ∈ ↑S), x ≤ ⟨y, y_S⟩

theorem ZFSet.Min_mem (S : ZFFinSet) [linord : LinearOrder ↥↑S] (nempS : (↑S).Nonempty) : (↑S).Min ∈ ↑S

theorem ZFSet.Min_spec {S : ZFFinSet} [linord : LinearOrder ↥↑S] (nempS : (↑S).Nonempty) (y : ↥↑S) : ⟨(↑S).Min, ⋯⟩ ≤ y

theorem ZFSet.Max_exists {S : ZFFinSet} [linord : LinearOrder ↥↑S] (nempS : (↑S).Nonempty) : ∃ (x : ↥↑S), ∀ (y : ↥↑S), y ≤ x

theorem ZFSet.Max_mem (S : ZFFinSet) [linord : LinearOrder ↥↑S] (nempS : (↑S).Nonempty) : (↑S).Max ∈ ↑S

theorem ZFSet.Max_spec {S : ZFFinSet} [linord : LinearOrder ↥↑S] (nempS : (↑S).Nonempty) (y : ↥↑S) : ⟨(↑S).Max, ⋯⟩ ≤ y

noncomputable def ZFSet.get (x : ZFSet.{u_1}) (n : ℕ) (i : Fin n) : ZFSet.{u_1}

Equations

• x.get 1 i_2 = x
• x.get n_2.succ.succ i_2 = if h : i_2 = Fin.last (n_2 + 1) then x.π₂ else x.π₁.get (n_2 + 1) (i_2.castPred h)

def ZFSet.hasArity (x : ZFSet.{u_1}) (n : ℕ) : Prop

Equations

• x.hasArity 0 = False
• x.hasArity 1 = True
• x.hasArity n_2.succ = if ∃ (a : ZFSet.{?u.3}) (b : ZFSet.{?u.3}), x = a.pair b then x.π₁.hasArity n_2 else False

theorem ZFSet.isTuple_pair {a b : ZFSet.{u_1}} : (a.pair b).hasArity 2

theorem ZFSet.sep_mem_powerset {D T : ZFSet.{u_1}} {P : ZFSet.{u_1} → Prop} : D ∈ T.powerset → ZFSet.sep P D ∈ T.powerset

theorem ZFSet.subset_of_𝔹_sInter (B : ZFSet.{u_1}) : B ⊆ 𝔹 → B.sInter ∈ 𝔹

theorem ZFSet.subset_of_𝔹_sUnion (B : ZFSet.{u_1}) : B ⊆ 𝔹 → B.sUnion ∈ 𝔹

theorem ZFSet.sInter_sep_subset_of_𝔹_mem_𝔹 {D : ZFSet.{u_1}} {P : ZFSet.{u_1} → Prop} : D ⊆ 𝔹 → (ZFSet.sep P D).sInter ∈ 𝔹

theorem ZFSet.sUnion_sep_subset_of_𝔹_mem_𝔹 {D : ZFSet.{u_1}} {P : ZFSet.{u_1} → Prop} : D ⊆ 𝔹 → (ZFSet.sep P D).sUnion ∈ 𝔹

theorem ZFSet.IsFunc.sep_on_eq {A B : ZFSet.{u_1}} {f : ZFSet.{u_1} → ZFSet.{u_1}} (hf : ∀ x ∈ A, f x ∈ B) : A.IsFunc B (ZFSet.sep (fun (z : ZFSet.{u_1}) => ∃ (x : ZFSet.{u_1}) (y : ZFSet.{u_1}), z = x.pair y ∧ y = f z.π₁) (A.prod B))

theorem ZFSet.IsFunc.is_func_on_range {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) : A.IsFunc (f.Range ⋯) f

theorem ZFSet.IsPFunc.empty_dom {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) (dom_emp : f.Dom ⋯ = ∅) : f = ∅

theorem ZFSet.IsPFunc.empty_range_of_empty_dom {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) (dom_emp : f.Dom ⋯ = ∅) : f.Range ⋯ = ∅

theorem ZFSet.IsPFunc.exists_dom_of_mem_range {f A B : ZFSet.{u_1}} (hf : f.IsPFunc A B) {y : ZFSet.{u_1}} (hy : y ∈ f.Range ⋯) : ∃ x ∈ A, x.pair y ∈ f

theorem ZFSet.IsFunc.surj_on_range {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) : f.IsSurjective ⋯

theorem ZFSet.bijective_of_injective {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) (inj : f.IsInjective hf) : f.IsBijective ⋯

theorem ZFSet.IsFunc.range_eq_of_surjective {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) (surj : f.IsSurjective hf) : f.Range ⋯ = B

@[reducible]

def ZFSet.instPreorder_mem_Nat {n : ZFSet.{u_1}} (hn : n ∈ Nat) : Preorder ↥n

Equations

• One or more equations did not get rendered due to their size.

theorem ZFSet.IsFinite.empty : ∅.IsFinite

theorem ZFSet.IsFinite.subset {A B : ZFSet.{u_1}} (finB : B.IsFinite) (subAB : A ⊆ B) : A.IsFinite

theorem ZFSet.IsFinite.insert {A : ZFSet.{u_1}} (finA : A.IsFinite) (x : ZFSet.{u_1}) : (Insert.insert x A).IsFinite

theorem ZFSet.IsFinite.disjoint_union {A B : ZFSet.{u_1}} (finA : A.IsFinite) (finB : B.IsFinite) (disjoint : A ∩ B = ∅) : (A ∪ B).IsFinite

theorem ZFSet.IsFinite.union {A B : ZFSet.{u_1}} (finA : A.IsFinite) (finB : B.IsFinite) : (A ∪ B).IsFinite

theorem ZFSet.IsFinite.inter {A B : ZFSet.{u_1}} (fin : A.IsFinite ∨ B.IsFinite) : (A ∩ B).IsFinite

theorem ZFSet.IsFinite.diff {A B : ZFSet.{u_1}} (finA : A.IsFinite) : (A \ B).IsFinite

def ZFSet.ZFFinSet.inductionOn {P : ZFFinSet → Prop} (empty : P ⟨∅, IsFinite.empty⟩) (insert : ∀ (S : ZFFinSet) (x : ZFSet.{u_1}), P S → x ∉ ↑S → P ⟨insert x ↑S, ⋯⟩) (S : ZFFinSet) : P S

Equations

• ⋯ = ⋯

theorem ZFSet.IsFinite.singleton {x : ZFSet.{u_1}} : {x}.IsFinite

theorem ZFSet.IsFinite.prod_singleton {A x : ZFSet.{u_1}} (finA : A.IsFinite) : (A.prod {x}).IsFinite

theorem ZFSet.IsFinite.singleton_prod {A x : ZFSet.{u_1}} (finA : A.IsFinite) : ({x}.prod A).IsFinite

theorem ZFSet.IsFinite.prod {A B : ZFSet.{u_1}} (finA : A.IsFinite) (finB : B.IsFinite) : (A.prod B).IsFinite

theorem ZFSet.IsFinite.sep {A : ZFSet.{u_1}} (finA : A.IsFinite) (P : ZFSet.{u_1} → Prop) : (ZFSet.sep P A).IsFinite

theorem ZFSet.ZFNat.every_nat_isfinite (n : ZFNat) : (↑n).IsFinite

theorem ZFSet.IsFinite.exists_bij {A : ZFSet.{u_1}} (finA : A.IsFinite) : ∃ (n : ZFSet.{u_1}) (f : ZFSet.{u_1}) (_ : n ∈ Nat) (hf : f ∈ A.funs n), f.IsBijective ⋯

noncomputable def ZFSet.Card : ZFFinSet → ZFNat

Equations

• ZFSet.Card ⟨S, Sfin⟩ = if S = ∅ then 0 else have ex_bij := ⋯; ⟨Classical.choose ex_bij, ⋯⟩

@[simp]

theorem ZFSet.Card.empty_iff {S : ZFFinSet} : Card S = 0 ↔ S = ⟨∅, IsFinite.empty⟩

@[simp]

theorem ZFSet.Card.empty : Card ⟨∅, IsFinite.empty⟩ = 0

@[simp]

theorem ZFSet.Card.singleton (x : ZFSet.{u_1}) : Card ⟨{x}, ⋯⟩ = 1

theorem ZFSet.Card.insert {S : ZFFinSet} {x : ZFSet.{u_1}} (hx : x ∉ ↑S) : Card ⟨Insert.insert x ↑S, ⋯⟩ = Card S + 1

def ZFSet.Card.inductionOn {P : ZFFinSet → Prop} (zero : P ⟨∅, IsFinite.empty⟩) (succ : ∀ (n : ZFNat), (∀ (S : ZFFinSet), n = Card S → P S) → ∀ (S' : ZFFinSet), Card S' = n + 1 → P S') (S : ZFFinSet) : P S

Equations

• ⋯ = ⋯

theorem ZFSet.IsFinite.powerset {A : ZFSet.{u_1}} (finA : A.IsFinite) : A.powerset.IsFinite

theorem ZFSet.IsFinite.finite_funs (S T : ZFSet.{u_1}) (finS : S.IsFinite) (finT : T.IsFinite) : (S.funs T).IsFinite

theorem ZFSet.IsFinite.exists_bij_mono_iff {S : ZFSet.{u_1}} [inst : Preorder ↥S] : S.IsFinite ↔ ∃ (n : ZFSet.{u_1}) (f : ZFSet.{u_1}) (x : n ∈ Nat) (hf : f ∈ S.funs n), f.IsBijective ⋯ ∧ IsStrictMono ⋯

theorem ZFSet.Min_mem_of_non_empty_finite {S : ZFSet.{u_1}} [inst : LinearOrder ↥S] (S_nemp : S.Nonempty) (S_fin : S.IsFinite) : S.Min ∈ S

theorem ZFSet.image_of_lambda_subset_range {A B φ : ZFSet.{u_1}} {hφ : A.IsFunc B φ} {S : ZFSet.{u_1}} : (φ[S]) ⋯ ⊆ B

noncomputable def ZFSet.fprod {A B A' B' : ZFSet.{u_1}} (f g : ZFSet.{u_1}) (hf : A.IsFunc A' f := by zfun) (hg : B.IsFunc B' g := by zfun) : ZFSet.{u_1}

Equations

• One or more equations did not get rendered due to their size.

theorem ZFSet.fprod_is_func {A B A' B' φ ψ : ZFSet.{u_1}} (hφ : A.IsFunc A' φ) (hψ : B.IsFunc B' ψ) : (A.prod B).IsFunc (A'.prod B') (fprod φ ψ hφ hψ)

theorem ZFSet.fprod_bijective_of_bijective {A B A' B' φ ψ : ZFSet.{u_1}} {hφ : A.IsFunc A' φ} {hψ : B.IsFunc B' ψ} (φ_bij : φ.IsBijective hφ) (ψ_bij : ψ.IsBijective hψ) : (fprod φ ψ hφ hψ).IsBijective ⋯

theorem ZFSet.mem_fprod {A B C D f g x : ZFSet.{u_1}} {hf : A.IsFunc C f} {hg : B.IsFunc D g} : x ∈ fprod f g hf hg ↔ ∃ (a : ZFSet.{u_1}) (b : ZFSet.{u_1}) (ha : a ∈ A) (hb : b ∈ B), have fa := ↑(@ᶻf ⋯ ⟨a, ⋯⟩); have gb := ↑(@ᶻg ⋯ ⟨b, ⋯⟩); x = (a.pair b).pair (fa.pair gb)

theorem ZFSet.pair_mem_fprod {A B C D f g x y : ZFSet.{u_1}} {hf : A.IsFunc C f} {hg : B.IsFunc D g} : x.pair y ∈ fprod f g hf hg ↔ ∃ (a : ZFSet.{u_1}) (b : ZFSet.{u_1}) (ha : a ∈ A) (hb : b ∈ B), have fa := ↑(@ᶻf ⋯ ⟨a, ⋯⟩); have gb := ↑(@ᶻg ⋯ ⟨b, ⋯⟩); x = a.pair b ∧ y = fa.pair gb

@[simp]

theorem ZFSet.fapply_fprod {A B C D f g a b : ZFSet.{u_1}} (hf : A.IsFunc C f) (hg : B.IsFunc D g) (ha : a ∈ A) (hb : b ∈ B) : ↑(@ᶻ(fprod f g hf hg) ⋯ ⟨a.pair b, ⋯⟩) = have fa := ↑(@ᶻf ⋯ ⟨a, ⋯⟩); have gb := ↑(@ᶻg ⋯ ⟨b, ⋯⟩); fa.pair gb

theorem ZFSet.composition_fprod_Image_bijective {A B A' B' φ ψ : ZFSet.{u_1}} {hφ : A.IsFunc A' φ} {hψ : B.IsFunc B' ψ} (φ_bij : φ.IsBijective hφ) (ψ_bij : ψ.IsBijective hψ) : let φ_ψ := fprod φ ψ hφ hψ; have φ_ψ_bij := ⋯; have Φ := (A.prod B).powerset.lambda (A'.prod B').powerset fun (a : ZFSet.{u_1}) => (φ_ψ[a]) ⋯; ∃ (hΦ : (A.prod B).powerset.IsFunc (A'.prod B').powerset Φ), Φ.IsBijective hΦ

theorem ZFSet.fprod_injective_of_injective {A B A' B' φ ψ : ZFSet.{u_1}} {hφ : A.IsFunc A' φ} {hψ : B.IsFunc B' ψ} (φ_inj : φ.IsInjective hφ) (ψ_inj : ψ.IsInjective hψ) : (fprod φ ψ hφ hψ).IsInjective ⋯