norm_of_subsingleton' — Mathlib

English

If E is a subsingleton, then ∥a∥ = 0 for every a ∈ E.

Русский

Если E — подсубмножество (одиночное множество), то для любого a ∈ E выполняется ∥a∥ = 0.

LaTeX

$$$[\text{Subsingleton } E]\Rightarrow \forall a\in E,\|a\| = 0$$$

Lean4

@[to_additive (attr := nontriviality) norm_of_subsingleton]
theorem norm_of_subsingleton' [Subsingleton E] (a : E) : ‖a‖ = 0 := by rw [Subsingleton.elim a 1, norm_one']

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