intrinsicClosure_mono — Mathlib

English

If s ⊆ t, then the intrinsic closure of s is contained in the intrinsic closure of t.

Русский

Если $s \subseteq t$, то внутреннее замыкание $s$ содержится в внутреннем замыкании $t$.

LaTeX

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

Lean4

theorem intrinsicClosure_mono (h : s ⊆ t) : intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t :=
  by
  refine image_subset_iff.2 fun x hx => ?_
  refine ⟨Set.inclusion (affineSpan_mono _ h) x, ?_, rfl⟩
  refine (continuous_inclusion (affineSpan_mono _ h)).closure_preimage_subset _ (closure_mono ?_ hx)
  exact fun y hy => h hy

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