finiteSubspace — Mathlib

English

The subspace of vectors with finite ENormedSpace norm is {x | e x < ∞}.

Русский

Подпространство векторов с конечной нормой задано как {x | e(x) < ∞}.

LaTeX

$$def finiteSubspace : Subspace 𝕜 V where carrier := {x | e x < ∞}$$

Lean4

/-- The subspace of vectors with finite ENormedSpace. -/
@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]
def finiteSubspace : Subspace 𝕜 V where
  carrier := {x | e x < ⊤}
  zero_mem' := by simp
  add_mem' {x y} hx hy := lt_of_le_of_lt (e.map_add_le x y) (ENNReal.add_lt_top.2 ⟨hx, hy⟩)
  smul_mem' c x
    (hx : _ < _) :=
    calc
      e (c • x) = ‖c‖₊ * e x := e.map_smul c x
      _ < ⊤ := ENNReal.mul_lt_top ENNReal.coe_lt_top hx

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