eq_one_iff — Mathlib

English

If v and w are equivalent absolute values, then for every x we have 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) = 1 \iff w(x) = 1 $$$

Lean4

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

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