sumLexAssoc_apply_inl_inl — Mathlib

English

Lexicographic sums preserve associativity via an order isomorphism; sumLexAssoc α β γ : (α ⊕ₗ β) ⊕ₗ γ ≃o α ⊕ₗ β ⊕ₗ γ.

Русский

Лексикографическая сумма сохраняет ассоциативность через порядок-изоморфизм: sumLexAssoc α β γ : (α ⊕ₗ β) ⊕ₗ γ ≃o α ⊕ₗ β ⊕ₗ γ.

LaTeX

$$$\text{sumLexAssoc }(\alpha,\beta,\gamma) : (\alpha \oplus_\mathrm{lex} \beta) \oplus_\mathrm{lex} \gamma \cong_o \alpha \oplus_\mathrm{lex} (\beta \oplus_\mathrm{lex} \gamma)$$$

Lean4

@[simp]
theorem sumLexAssoc_apply_inl_inl : sumLexAssoc α β γ (toLex <| inl <| toLex <| inl a) = toLex (inl a) :=
  rfl

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