LeanPool.ZFLean.IsomorphismsZFNatIso

Imported Lean Pool material for LeanPool.ZFLean.IsomorphismsZFNatIso.

@[reducible, inline]

noncomputable abbrev ZFSet.ZFNat.deletePointIsoMap (k : ZFNat) (ℓ : ZFSet.{u_1}) : ZFSet.{u_1}

The map identifying k with (k + 1) \ {ℓ} for ℓ ∈ k + 1.

Equations

• k.deletePointIsoMap ℓ = ZFSet.sep (fun (xy : ZFSet.{?u.1}) => have x := xy.π₁; have y := xy.π₂; if x ∈ ℓ then x = y else y = insert x x) ((↑k).prod (↑(k + 1) \ {ℓ}))

theorem ZFSet.ZFNat.deletePointIsoMap_isFunc {k : ZFNat} {ℓ : ZFSet.{u_1}} : (↑k).IsFunc (↑(k + 1) \ {ℓ}) (k.deletePointIsoMap ℓ)

theorem ZFSet.ZFNat.deletePointIsoMap_bijective {k : ZFNat} {ℓ : ZFSet.{u_1}} (ℓ_mem_m : ℓ ∈ ↑(k + 1)) : (k.deletePointIsoMap ℓ).IsBijective ⋯

theorem ZFSet.ZFNat.isIso_delete_singleton {k : ZFNat} {ℓ : ZFSet.{u_1}} (ℓ_mem_m : ℓ ∈ ↑(k + 1)) : ↑k ≅ᶻ ↑(k + 1) \ {ℓ}

theorem ZFSet.ZFNat.iso_eq_iff_proof {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m

Imported ZFLean declaration.

theorem ZFSet.ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m