span_univ — Mathlib

English

The span of the entire projective space is the top of the lattice of subspaces.

Русский

Область всего проективного пространства смоделирована как верхняя граница подпространств.

LaTeX

$$$\operatorname{span}(\mathbb{P}_K V) = \top$$$

Lean4

/-- The span of the entire projective space is the top of the lattice of subspaces. -/
@[simp]
theorem span_univ : span (Set.univ : Set (ℙ K V)) = ⊤ :=
  by
  rw [eq_top_iff, SetLike.le_def]
  intro x _hx
  exact subset_span _ (Set.mem_univ x)

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