toRelIsoLT — Mathlib

English

An order isomorphism e between α and β induces a RelIso between the less-than relations on α and β.

Русский

Упорядоченное изоморфизм e между α и β индуцирует RelIso между отношениями < на α и β.

LaTeX

$$$((\cdot < \cdot) : \alpha \to \alpha \to \mathrm{Prop}) \cong_r ((\cdot < \cdot) : \beta \to \beta \to \mathrm{Prop})$$$

Lean4

/-- Converts an `OrderIso` into a `RelIso (<) (<)`. -/
def toRelIsoLT (e : α ≃o β) : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop) :=
  ⟨e.toEquiv, lt_iff_lt e⟩

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