lt_iff_lt — Mathlib

English

Equivalence preserves the less-than relation: v1 x < v1 y iff v2 x < v2 y when v1 ≈ v2.

Русский

Эквивалентность сохраняет отношение «меньше»: v1 x < v1 y эквивалентно v2 x < v2 y при v1 ≈ v2.

LaTeX

$$$ (v_1 \IsEquiv v_2) \rightarrow \forall x,y:\, R, v_1(x) < v_1(y) \iff v_2(x) < v_2(y) $$$

Lean4

theorem lt_iff_lt (h : v₁.IsEquiv v₂) {x y : R} : v₁ x < v₁ y ↔ v₂ x < v₂ y := by rw [← le_iff_le_iff_lt_iff_lt, h]

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