span_eq_sInf — Mathlib

English

The span of a set equals the infimum of all subspaces that contain the set.

Русский

Span множества равен инфиминуму всех подпространств, содержащих это множество.

LaTeX

$$$\operatorname{span}(S) = \inf\{W : \mathrm{Subspace}(K,V) \mid S \subseteq W\}$$$

Lean4

/-- The span of a set of points in a projective space is equal to the infimum of the collection of
subspaces which contain the set. -/
theorem span_eq_sInf {S : Set (ℙ K V)} : span S = sInf {W : Subspace K V | S ⊆ W} :=
  by
  ext x
  simp_rw [mem_carrier_iff, mem_span x]
  refine ⟨fun hx => ?_, fun hx W hW => ?_⟩
  · rintro W ⟨T, hT, rfl⟩
    exact hx T hT
  · exact (@sInf_le _ _ {W : Subspace K V | S ⊆ ↑W} W hW) hx

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