isNontrivial_iff_ne_trivial — Mathlib

English

An absolute value is nontrivial iff it is not equal to the trivial absolute value.

Русский

Абсолютная величина ненулевый эквивалентно не тривиальной величине.

LaTeX

$$$v.IsNontrivial \\iff v \\neq \\operatorname{AbsoluteValue.trivial}$$$

Lean4

theorem isNontrivial_iff_ne_trivial [DecidablePred fun x : R ↦ x = 0] [NoZeroDivisors R] [Nontrivial S]
    (v : AbsoluteValue R S) : v.IsNontrivial ↔ v ≠ .trivial :=
  by
  refine ⟨fun ⟨x, hx₀, hx₁⟩ h ↦ hx₁ <| h.symm ▸ trivial_apply hx₀, fun H ↦ ?_⟩
  simp only [IsNontrivial]
  contrapose! H
  ext1 x
  rcases eq_or_ne x 0 with rfl | hx
  · simp
  · simp [H, hx]

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