affineSpan_intrinsicClosure — Mathlib

English

The affine span of intrinsicClosure(s) equals the affine span of s.

Русский

Аффинное пространство, порожденное intrinsicClosure(s), равно affineSpan(s).

LaTeX

$$affineSpan_{\\mathbb{k}}(intrinsicClosure_{\\mathbb{k}}(s)) = affineSpan_{\\mathbb{k}}(s)$$

Lean4

@[simp]
theorem affineSpan_intrinsicClosure (s : Set P) : affineSpan 𝕜 (intrinsicClosure 𝕜 s) = affineSpan 𝕜 s :=
  (affineSpan_le.2 intrinsicClosure_subset_affineSpan).antisymm <| affineSpan_mono _ subset_intrinsicClosure

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