sumAssoc — Mathlib

English

Sum of types is associative up to a natural equivalence: (α ⊕ β) ⊕ γ ≃ α ⊕ (β ⊕ γ).

Русский

Сумма типов ассоциативна до естественной эквивалентности: (α ⊕ β) ⊕ γ ≃ α ⊕ (β ⊕ γ).

LaTeX

$$$$(\alpha \oplus \beta) \oplus \gamma \simeq \alpha \oplus (\beta \oplus \gamma).$$$$

Lean4

/-- Sum of types is associative up to an equivalence. -/
def sumAssoc (α β γ) : (α ⊕ β) ⊕ γ ≃ α ⊕ (β ⊕ γ) :=
  ⟨Sum.elim (Sum.elim Sum.inl (Sum.inr ∘ Sum.inl)) (Sum.inr ∘ Sum.inr),
    Sum.elim (Sum.inl ∘ Sum.inl) <| Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr, by rintro (⟨_ | _⟩ | _) <;> rfl, by
    rintro (_ | ⟨_ | _⟩) <;> rfl⟩

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