English
If v and w are two nontrivial inequivalent absolute values, then there exists a with 1 < v(a) and w(a) < 1.
Русский
Если v и w не тривиальны и не эквивалентны, то существует a, для которого 1 < v(a) и w(a) < 1.
LaTeX
$$$ v.IsNontrivial \land w.IsNontrivial \land \lnot (v IsEquiv w) \Rightarrow \exists a, 1 < v(a) \land w(a) < 1 $$$
Lean4
/-- If `v` and `w` are two non-trivial and inequivalent absolute values then we can find an `a : R`
such that `1 < v a` while `w a < 1`.
-/
theorem exists_one_lt_lt_one_of_not_isEquiv {v w : AbsoluteValue R S} (hv : v.IsNontrivial) (hw : w.IsNontrivial)
(h : ¬v.IsEquiv w) : ∃ a : R, 1 < v a ∧ w a < 1 :=
by
let ⟨a, hva, hwa⟩ := exists_lt_one_one_le_of_not_isEquiv hv h
let ⟨b, hwb, hvb⟩ := exists_lt_one_one_le_of_not_isEquiv hw (mt .symm h)
exact
⟨b / a, by
simp [w.pos_iff.1 (lt_of_lt_of_le zero_lt_one hwa), one_lt_div, div_lt_one, lt_of_le_of_lt' hvb hva,
lt_of_le_of_lt' hwa hwb]⟩
