intrinsicClosure — Mathlib

English

If the preimage of s under the affine inclusion is closed, then intrinsicClosure(s) = s.

Русский

Если предобразование s по включению в аффинное пространство замкнуто, то intrinsicClosure(s) = s.

LaTeX

$$IsClosed((incl)^{-1}(s)) \\Rightarrow intrinsicClosure_{\\mathbb{k}}(s) = s$$

Lean4

protected theorem intrinsicClosure (hs : IsClosed ((↑) ⁻¹' s : Set <| affineSpan 𝕜 s)) : intrinsicClosure 𝕜 s = s :=
  by
  rw [intrinsicClosure, hs.closure_eq, image_preimage_eq_of_subset]
  exact (subset_affineSpan _ _).trans Subtype.range_coe.superset

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