nullSubmodule — Mathlib

English

The nullSubmodule 𝕜 E is the subspace { x ∈ E : ∥x∥ = 0 }.

Русский

nullSubmodule 𝕜 E есть подпространство { x ∈ E : ∥x∥ = 0 }.

LaTeX

$$$nullSubmodule(\mathbb{K},E)=\{x\in E : \|x\|=0\}$$$

Lean4

/-- The null space with respect to the norm. -/
def nullSubmodule : Submodule 𝕜 E where
  __ := nullAddSubgroup E
  smul_mem' c x
    (hx : ‖x‖ = 0) := by
    apply le_antisymm _ (norm_nonneg _)
    refine (norm_smul_le _ _).trans_eq ?_
    rw [hx, mul_zero]

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