boolEquivPUnitSumPUnit — Mathlib

English

Bool is equivalent to the sum of two PUnits: Bool ≃ PUnit_{u+1} ⊕ PUnit_{v+1}.

Русский

Bool эквивалентен сумме двух PUnit: Bool ≃ PUnit_{u+1} ⊕ PUnit_{v+1}.

LaTeX

$$def boolEquivPUnitSumPUnit : Bool ≃ PUnit.{u + 1} ⊕ PUnit.{v + 1}$$

Lean4

/-- `Bool` is equivalent the sum of two `PUnit`s. -/
def boolEquivPUnitSumPUnit : Bool ≃ PUnit.{u + 1} ⊕ PUnit.{v + 1} :=
  ⟨fun b => b.casesOn (inl PUnit.unit) (inr PUnit.unit), Sum.elim (fun _ => false) fun _ => true, fun b => by
    cases b <;> rfl, fun s => by rcases s with (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> rfl⟩

Похожие утверждения