le_one_iff — Mathlib

English

Let v and w be equivalent absolute values on a semiring with appropriate domain. Then for every x, v(x) ≤ 1 if and only if w(x) ≤ 1.

Русский

Пусть v и w — эквивалентные абсолютные значения на полусуществе; тогда для каждого x выполняется v(x) ≤ 1 тогда и только тогда, когда w(x) ≤ 1.

LaTeX

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

Lean4

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

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