Isomorphisms of ZF sets #

This file develops the theory of isomorphisms (bijections) between ZF sets, including the Cantor–Bernstein theorem, isomorphism stability under products, powersets and function spaces, and currying/uncurrying.

source

def ZFSet.isIso (A B : ZFSet.{u_1}) :

Prop

Equations

(A ≅ᶻ B) = ∃ (bij : ZFSet.{?u.1}) (is_func : A.IsFunc B bij), bij.IsBijective is_func

Instances For

source

def ZFSet.«term_≅ᶻ_» :

Lean.TrailingParserDescr

Equations

ZFSet.«term_≅ᶻ_» = Lean.ParserDescr.trailingNode `ZFSet.«term_≅ᶻ_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≅ᶻ ") (Lean.ParserDescr.cat `term 41))

Instances For

source

theorem ZFSet.isIso_refl (A : ZFSet.{u_1}) :

A ≅ᶻ A

source

@[implicit_reducible]

instance ZFSet.instTransIsIso :

Trans isIso isIso isIso

Equations

ZFSet.instTransIsIso = { trans := @ZFSet.instTransIsIso._proof_1 }

source

theorem ZFSet.isIso_symm ⦃x y : ZFSet.{u_1}⦄ :

x ≅ᶻ y → y ≅ᶻ x

source

instance ZFSet.instSymmIsIso :

Std.Symm isIso

source

theorem ZFSet.isIso_trans ⦃x y z : ZFSet.{u_1}⦄ :

x ≅ᶻ y → y ≅ᶻ z → x ≅ᶻ z

source

instance ZFSet.instIsTransIsIso :

IsTrans ZFSet.{u_1} isIso

source

theorem ZFSet.isIso_equiv :

Equivalence isIso

source

instance ZFSet.instIsEquivIsIso :

IsEquiv ZFSet.{u_1} isIso

source

theorem ZFSet.bijective_of_injective_on_subset {A B : ZFSet.{u_1}} (B_sub : B ⊆ A) {u : ZFSet.{u_1}} {hu : A.IsFunc B u} (u_inj : u.IsInjective hu) :

∃ (v : ZFSet.{u_1}) (hv : A.IsFunc B v), v.IsBijective hv

source

theorem ZFSet.isIso_of_biembedding {E F f g : ZFSet.{u_1}} {hf : E.IsFunc F f} (f_inj : f.IsInjective hf) {hg : F.IsFunc E g} (g_inj : g.IsInjective hg) :

E ≅ᶻ F

Cantor–Bernstein theorem: if there are injective functions f : A → B and g : B → A, then A and B are isomorphic.

source

theorem ZFSet.schroeder_bernstein {E F f g : ZFSet.{u_1}} {hf : E.IsFunc F f} (f_inj : f.IsInjective hf) {hg : F.IsFunc E g} (g_inj : g.IsInjective hg) :

E ≅ᶻ F

Alias of ZFSet.isIso_of_biembedding.

Cantor–Bernstein theorem: if there are injective functions f : A → B and g : B → A, then A and B are isomorphic.

source

theorem ZFSet.isIso_of_prod {A B C D : ZFSet.{u_1}} (h : A ≅ᶻ C) (h' : B ≅ᶻ D) :

A.prod B ≅ᶻ C.prod D

source

theorem ZFSet.inv_Image_of_bijective {f A B : ZFSet.{u_1}} {hf : A.IsFunc B f} (bij : f.IsBijective hf) {X : ZFSet.{u_1}} (hX : X ⊆ A) :

((f⁻¹ ⋯)[(f[X]) ⋯]) ⋯ = X

source

theorem ZFSet.Image_inv_of_bijective {f A B : ZFSet.{u_1}} {hf : A.IsFunc B f} (bij : f.IsBijective hf) {X : ZFSet.{u_1}} (hX : X ⊆ B) :

(f[((f⁻¹ ⋯)[X]) ⋯]) ⋯ = X

source

theorem ZFSet.IsInjective_of_left_inverse {A B f : ZFSet.{u_1}} (hf : A.IsFunc B f) {g : ZFSet.{u_1}} (hg : B.IsFunc A g) (left_inv : (g ∘ᶻ f) hg hf = 𝟙A) :

f.IsInjective hf

source

theorem ZFSet.IsSurjective_of_right_inverse {A B f : ZFSet.{u_1}} (hf : A.IsFunc B f) {g : ZFSet.{u_1}} (hg : B.IsFunc A g) (right_inv : (f ∘ᶻ g) hf hg = 𝟙B) :

f.IsSurjective hf

source

theorem ZFSet.isIso_of_two_sided_inverse {A B f : ZFSet.{u_1}} {hf : A.IsFunc B f} {g : ZFSet.{u_1}} {hg : B.IsFunc A g} (left_inv : (g ∘ᶻ f) hg hf = 𝟙A) (right_inv : (f ∘ᶻ g) hf hg = 𝟙B) :

A ≅ᶻ B

source

theorem ZFSet.isIso_powerset {A B : ZFSet.{u_1}} (h : A ≅ᶻ B) :

A.powerset ≅ᶻ B.powerset

source

theorem ZFSet.isIso_funs_to_pow_rel {A B : ZFSet.{u_1}} :

A.funs B.powerset ≅ᶻ (A.prod B).powerset

source

theorem ZFSet.isIso_of_funs {A B C D : ZFSet.{u_1}} (h : A ≅ᶻ C) (h' : B ≅ᶻ D) :

A.funs B ≅ᶻ C.funs D

source

theorem ZFSet.isIso_powerset_char_pred {A : ZFSet.{u_1}} :

A.powerset ≅ᶻ A.funs 𝔹

source

theorem ZFSet.ZFNat.iso_eq_iff {n m : ZFNat} :

↑n ≅ᶻ ↑m ↔ n = m

source

noncomputable def ZFSet.currify {A B C : ZFSet.{u_1}} (f : ZFSet.{u_1}) (hf : (A.prod B).IsFunc C f := by zfun) :

ZFSet.{u_1}

Equations

ZFSet.currify f hf = A.lambda (B.funs C) fun (a : ZFSet.{?u.1}) => if ha : a ∈ A then B.lambda C fun (a_1 : ZFSet.{?u.1}) => if hb : a_1 ∈ B then ↑(@ᶻf ⋯ ⟨a.pair a_1, ⋯⟩) else ∅ else ∅

Instances For

source

theorem ZFSet.currify_is_func {A B C : ZFSet.{u_1}} (f : ZFSet.{u_1}) (hf : (A.prod B).IsFunc C f := by zfun) :

A.IsFunc (B.funs C) (currify f hf)

source

noncomputable def ZFSet.uncurrify {A B C : ZFSet.{u_1}} (g : ZFSet.{u_1}) (hg : A.IsFunc (B.funs C) g := by zfun) :

ZFSet.{u_1}

Equations

ZFSet.uncurrify g hg = (A.prod B).lambda C fun (a : ZFSet.{?u.1}) => if hab : a.π₁ ∈ A ∧ a.π₂ ∈ B then let f := @ᶻg ⋯ ⟨a.π₁, ⋯⟩; have hf := ⋯; ↑(@ᶻ↑f ⋯ ⟨a.π₂, ⋯⟩) else ∅

Instances For

source

theorem ZFSet.uncurrify_is_func {A B C : ZFSet.{u_1}} (g : ZFSet.{u_1}) (hg : A.IsFunc (B.funs C) g := by zfun) :

(A.prod B).IsFunc C (uncurrify g hg)

source

@[simp]

theorem ZFSet.currify_of_uncurrify {A B C : ZFSet.{u_1}} (f : ZFSet.{u_1}) (hf : A.IsFunc (B.funs C) f := by zfun) :

currify (uncurrify f hf) ⋯ = f

source

theorem ZFSet.uncurrify_of_currify {A B C : ZFSet.{u_1}} (g : ZFSet.{u_1}) (hg : (A.prod B).IsFunc C g := by zfun) :

uncurrify (currify g hg) ⋯ = g

source

theorem ZFSet.isIso_curry {A B C : ZFSet.{u_1}} :

(A.prod B).funs C ≅ᶻ A.funs (B.funs C)

Documentation

ZFLean.Isomorphisms

Isomorphisms of ZF sets #