exists_lt_one_one_le_of_not_isEquiv

English

If v is nontrivial and v is not equivalent to w, there exists a such that v(a) < 1 and 1 ≤ w(a).

Русский

Если v ненулевая и не эквивалентна w, существует a, для которого v(a) < 1 и 1 ≤ w(a).

LaTeX

$$$ v.IsNontrivial \land \lnot (v IsEquiv w) \Rightarrow \exists a, v(a) < 1 \land 1 \le w(a) $$$

Lean4

/-- If `v` and `w` are inequivalent absolute values and `v` is non-trivial, then we can find an `a : R`
such that `v a < 1` while `1 ≤ w a`.
-/
theorem exists_lt_one_one_le_of_not_isEquiv {v w : AbsoluteValue R S} (hv : v.IsNontrivial) (h : ¬v.IsEquiv w) :
    ∃ a : R, v a < 1 ∧ 1 ≤ w a := by
  contrapose! h
  exact isEquiv_of_lt_one_imp hv h

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