intrinsicClosure_subset_affineSpan

English

The intrinsic closure is contained in the affine span of s.

Русский

Внутреннее замыкание множества содержится в аффine-порождающем множество.

LaTeX

$$$\\operatorname{intrinsicClosure}_{\\mathbb{k}}(s) \\subseteq \\operatorname{affineSpan}_{\\mathbb{k}}(s)$$$

Lean4

theorem intrinsicClosure_subset_affineSpan : intrinsicClosure 𝕜 s ⊆ affineSpan 𝕜 s :=
  (image_subset_range _ _).trans Subtype.range_coe.subset

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