LeanPool.ZFLean.Sum

Imported Lean Pool material for LeanPool.ZFLean.Sum.

def ZFSet.Sum (A B : ZFSet.{u_1}) : Type (u_1 + 1)

Imported ZFLean declaration.

Equations

• (A ⊎ B) = ↥({↑ZFSet.ZFBool.false}.prod A ∪ {↑ZFSet.ZFBool.true}.prod B)

def ZFSet.«term_⊎_» : Lean.TrailingParserDescr

Imported ZFLean declaration.

Equations

• ZFSet.«term_⊎_» = Lean.ParserDescr.trailingNode `ZFSet.«term_⊎_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊎ ") (Lean.ParserDescr.cat `term 50))

def ZFSet.Sum.inl {A B : ZFSet.{u_1}} (a : ↥A) : A ⊎ B

Imported ZFLean declaration.

Equations

• ZFSet.Sum.inl a = ⟨(↑ZFSet.ZFBool.false).pair ↑a, ⋯⟩

def ZFSet.Sum.inr {A B : ZFSet.{u_1}} (b : ↥B) : A ⊎ B

Imported ZFLean declaration.

Equations

• ZFSet.Sum.inr b = ⟨(↑ZFSet.ZFBool.true).pair ↑b, ⋯⟩

theorem ZFSet.Sum.inl.injEq {A B : ZFSet.{u_1}} {x y : ↥A} : inl x = inl y ↔ x = y

theorem ZFSet.Sum.inr.injEq {A B : ZFSet.{u_1}} {x y : ↥B} : inr x = inr y ↔ x = y

theorem ZFSet.Sum.cases {A B : ZFSet.{u_1}} (x : A ⊎ B) : (↑x).π₂ ∈ A ∨ (↑x).π₂ ∈ B

noncomputable def ZFSet.Sum.casesOn {A B : ZFSet.{u}} {motive : A ⊎ B → Sort v} (x : A ⊎ B) (inl : (val : ↥A) → motive (inl val)) (inr : (val : ↥B) → motive (inr val)) : motive x

Imported ZFLean declaration.

Equations

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

@[simp]

theorem ZFSet.Sum.casesOn_of_inl {A B : ZFSet.{u_2}} {motive : A ⊎ B → Sort u_1} (a : ↥A) (inl_case : (val : ↥A) → motive (inl val)) (inr_case : (val : ↥B) → motive (inr val)) : casesOn (inl a) inl_case inr_case = inl_case a

@[simp]

theorem ZFSet.Sum.casesOn_of_inr {A B : ZFSet.{u_2}} {motive : A ⊎ B → Sort u_1} (a : ↥B) (inl_case : (val : ↥A) → motive (inl val)) (inr_case : (val : ↥B) → motive (inr val)) : casesOn (inr a) inl_case inr_case = inr_case a

noncomputable def ZFSet.Sum.instEquivSumSubtypeMem {A B : ZFSet.{u_1}} : A ⊎ B ≃ ↥A ⊕ ↥B

The equivalence between the ZF disjoint sum and Lean's subtype sum.

Equations

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

def ZFSet.Option (S : ZFSet.{u_1}) : Type (u_1 + 1)

Imported ZFLean declaration.

Equations

• S.Option = ({∅} ⊎ S)

instance ZFSet.instNonemptyOption {T : ZFSet.{u_1}} : Nonempty T.Option

@[reducible, inline]

abbrev ZFSet.Option.none {S : ZFSet.{u_1}} : S.Option

Imported ZFLean declaration.

Equations

• ZFSet.Option.none = ZFSet.Sum.inl ⟨∅, ZFSet.Option.none._proof_1⟩

@[reducible, inline]

abbrev ZFSet.Option.some {S : ZFSet.{u_1}} (x : ↥S) : S.Option

Imported ZFLean declaration.

Equations

• ZFSet.Option.some x = ZFSet.Sum.inr x

theorem ZFSet.Option.some_ne_none {S : ZFSet.{u_1}} (x : ↥S) : some x ≠ none

theorem ZFSet.Option.casesOn {S : ZFSet.{u_1}} (x : S.Option) : x = none ∨ ∃ (y : ↥S), x = some y

@[reducible, inline]

noncomputable abbrev ZFSet.Option.the {S : ZFSet.{u_1}} (S_nemp : S ≠ ∅) (x : S.Option) : ↥S

Imported ZFLean declaration.

Equations

• ZFSet.Option.the S_nemp x = if isNone : x = ZFSet.Option.none then ⟨(fun (x : ZFSet.{?u.1}) => Classical.epsilon fun (z : ZFSet.{?u.1}) => z ∈ x) S, ⋯⟩ else Classical.choose ⋯

noncomputable def ZFSet.Option.into {T : ZFSet.{u_1}} : T.Option → _root_.Option ↥T

Convert a set-theoretic option to a Lean option of members of the underlying set.

Equations

• x.into = if hx : x = ZFSet.Option.none then none else some (Classical.choose ⋯)

theorem ZFSet.Option.some.injEq {T : ZFSet.{u_1}} {x y : ↥T} : some x = some y ↔ x = y

theorem ZFSet.Option.some_val_injEq {T : ZFSet.{u_1}} {x y : ↥T} : ↑(some x) = ↑(some y) ↔ x = y

theorem ZFSet.Option.ne_none_is_some {T : ZFSet.{u_1}} (x : T.Option) : x ≠ none → ∃ (y : ↥T), x = some y

theorem ZFSet.Option.into.inj {T : ZFSet.{u_1}} : Function.Injective into

theorem ZFSet.Option.into.surj {T : ZFSet.{u_1}} : Function.Surjective into

theorem ZFSet.Option.into.bij {T : ZFSet.{u_1}} : Function.Bijective into

noncomputable def ZFSet.Option.EmbeddingZFOptionOption {T : ZFSet.{u_1}} : T.Option ↪ _root_.Option ↥T

Imported ZFLean declaration.

Equations

• ZFSet.Option.EmbeddingZFOptionOption = { toFun := ZFSet.Option.into, inj' := ⋯ }

noncomputable def ZFSet.Option.instEquivZFOptionOption {T : ZFSet.{u_1}} : T.Option ≃ _root_.Option ↥T

The equivalence between ZF options and Lean options over a subtype.

Equations

• ZFSet.Option.instEquivZFOptionOption = { toFun := ZFSet.Option.into, invFun := Function.invFun ZFSet.Option.into, left_inv := ⋯, right_inv := ⋯ }

def ZFSet.Option.outof {T : ZFSet.{u_1}} : _root_.Option ↥T → T.Option

Convert a Lean option of set members to the set-theoretic option encoding.

Equations

• ZFSet.Option.outof (some ⟨x_1, hx⟩) = ZFSet.Option.some ⟨x_1, hx⟩
• ZFSet.Option.outof none = ZFSet.Option.none

theorem ZFSet.Option.outof.inj {T : ZFSet.{u_1}} : Function.Injective outof

theorem ZFSet.Option.outof.surj {T : ZFSet.{u_1}} : Function.Surjective outof

theorem ZFSet.Option.outof.bij {T : ZFSet.{u_1}} : Function.Bijective outof

def ZFSet.Option.EmbeddingOptionZFOption {T : ZFSet.{u_1}} : _root_.Option ↥T ↪ T.Option

Imported ZFLean declaration.

Equations

• ZFSet.Option.EmbeddingOptionZFOption = { toFun := ZFSet.Option.outof, inj' := ⋯ }

noncomputable def ZFSet.Option.instEquivOptionZFOption {T : ZFSet.{u_1}} : _root_.Option ↥T ≃ T.Option

The equivalence between Lean options over a subtype and ZF options.

Equations

• ZFSet.Option.instEquivOptionZFOption = { toFun := ZFSet.Option.outof, invFun := Function.invFun ZFSet.Option.outof, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

abbrev ZFSet.Option.toZFSet (T : ZFSet.{u_1}) : ZFSet.{u_1}

Imported ZFLean declaration.

Equations

• ZFSet.Option.toZFSet T = {↑ZFSet.ZFBool.false}.prod {∅} ∪ {↑ZFSet.ZFBool.true}.prod T

noncomputable def ZFSet.Option.flift {A B : ZFSet.{u_1}} (f : ZFSet.{u_1}) (hf : A.IsFunc B f := by zfun) : { f' : ZFSet.{u_1} // (toZFSet A).IsFunc (toZFSet B) f' }

Imported ZFLean declaration.

Equations

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

theorem ZFSet.Option.flift_bijective {f A B : ZFSet.{u_1}} (hf : A.IsFunc B f) : (↑(flift f hf)).IsBijective ⋯ ↔ f.IsBijective hf