exists_norm_mul_eq_self — Mathlib

English

There exists a unit c with ||c|| = 1 such that c · ||x|| = x, with the trivial case x = 0 giving c = 1.

Русский

Существует единичный множитель c с ||c|| = 1 такой, что c · ||x|| = x; если x = 0, взять c = 1.

LaTeX

$$$$ \exists c, \|c\| = 1 \land c \cdot \|x\| = x. $$$$

Lean4

theorem exists_norm_mul_eq_self (x : K) : ∃ c, ‖c‖ = 1 ∧ c * ‖x‖ = x :=
  by
  obtain rfl | hx := eq_or_ne x 0
  · exact ⟨1, by simp⟩
  · exact ⟨x / ‖x‖, by simp [norm_ne_zero_iff.2, hx]⟩

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