sumComm — Mathlib

English

There is an order isomorphism swapping the two summands: Sum α β ≃o Sum β α, given by sumComm.

Русский

Существуют упорядоченные изоморфизмы, меняющие местами соммированные части: Sum α β ≃o Sum β α, задаваемый sumComm.

LaTeX

$$$\text{sumComm }(\alpha,\beta) : \alpha \oplus \beta \cong_o \beta \oplus \alpha$$$

Lean4

/-- `Equiv.sumComm` promoted to an order isomorphism. -/
@[simps! apply]
def sumComm (α β : Type*) [LE α] [LE β] : α ⊕ β ≃o β ⊕ α :=
  { Equiv.sumComm α β with map_rel_iff' := swap_le_swap_iff }

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