span_top — Mathlib

English

For a basis b in a normed space E over K, the span over K of the integer-span of the range of b equals the whole space: span_K(span_ℤ(range b)) = ⊤.

Русский

Для базиса b в нормированном пространстве E над полем K, линейная оболочка над K целиком равна ⊤: span_K(span_ℤ(range b)) = ⊤.

LaTeX

$$$\\operatorname{span}_K\\left(\\operatorname{span}_{\\mathbb{Z}}(\\operatorname{range} b)\\right) = \\top$$$

Lean4

theorem span_top : span K (span ℤ (Set.range b) : Set E) = ⊤ := by simp [span_span_of_tower]

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