lt_one_iff_lt_one — Mathlib

English

Equivalence implies the less-than-one relation is preserved: v1 x < 1 iff v2 x < 1 for all x.

Русский

Эквивлеченность сохраняет отношение меньше единицы: для всех x выполняется v1(x) < 1 ⇔ v2(x) < 1.

LaTeX

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

Lean4

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

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