norm_eq_zero_iff' — Mathlib

English

If x lies in the range of mixedEmbedding K, then mixedEmbedding.norm x = 0 if and only if x = 0.

Русский

Если x лежит в образе смешанного вложения, то ∥x∥ = 0 тогда и только тогда, когда x = 0.

LaTeX

$$$ x \in \mathrm{range}(\text{mixedEmbedding}(K)) \; \Rightarrow\; \|x\| = 0 \iff x = 0 $$$

Lean4

theorem norm_eq_zero_iff' {x : mixedSpace K} (hx : x ∈ Set.range (mixedEmbedding K)) :
    mixedEmbedding.norm x = 0 ↔ x = 0 := by
  obtain ⟨a, rfl⟩ := hx
  rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff, map_eq_zero]

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