exists_abv_lt_one — Mathlib

English

If v.IsNontrivial, there exists x ≠ 0 with v(x) < 1.

Русский

Если v.IsNontrivial, существует x ≠ 0 такое, что v(x) < 1.

LaTeX

$$$\\exists x \\neq 0, \\; \\operatorname{abv}(x) < 1$$$

Lean4

theorem exists_abv_lt_one (h : v.IsNontrivial) : ∃ x ≠ 0, v x < 1 :=
  by
  obtain ⟨y, hy⟩ := h.exists_abv_gt_one
  have hy₀ := v.ne_zero_iff.mp <| (zero_lt_one.trans hy).ne'
  refine ⟨y⁻¹, inv_ne_zero hy₀, ?_⟩
  rw [map_inv₀]
  exact (inv_lt_one₀ <| v.pos hy₀).mpr hy

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