ofRelIsoLT_apply — Mathlib

English

The application of the constructed order isomorphism to x equals the original RelIsoLT applied to x.

Русский

Применение построенного порядкового изоморфизма к x равно применению исходного RelIsoLT к x.

LaTeX

$$$ ofRelIsoLT\, e\, x = e\, x $$$

Lean4

@[simp]
theorem ofRelIsoLT_apply {α β} [PartialOrder α] [PartialOrder β]
    (e : ((· < ·) : α → α → Prop) ≃r ((· < ·) : β → β → Prop)) (x : α) : ofRelIsoLT e x = e x :=
  rfl

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