refl — Mathlib

English

The identity is the neutral element for the composition of order isomorphisms: refl trans f = f.

Русский

Тождественный изоморфизм порядка является нейтральным элементом при композиции: refl.trans f = f.

LaTeX

$$$\text{refl} : α \too α$, $(\text{refl } α) \trans f = f$.$$

Lean4

/-- The identity map as an ordered monoid isomorphism. -/
@[to_additive /-- The identity map as an ordered additive monoid isomorphism. -/
    ]
protected def refl : α ≃*o α :=
  { MulEquiv.refl α with map_le_map_iff' := by simp }

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