one_le_iff — Mathlib

English

If v and w are equivalent absolute values, then 1 ≤ v(x) holds exactly when 1 ≤ w(x) holds for any x.

Русский

Если v и w эквивалентны как абсолютные значения, то 1 ≤ v(x) эквивалично 1 ≤ w(x) для любого x.

LaTeX

$$$ (v \sim w) \Rightarrow \forall x,\ 1 \le v(x) \iff 1 \le w(x) $$$

Lean4

theorem one_le_iff (h : v.IsEquiv w) {x : R} : 1 ≤ v x ↔ 1 ≤ w x := by simpa only [map_one] using h 1 x

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