English
The intrinsic closure is equal to the topological closure (under standard hypotheses).
Русский
Внутреннее замыкание совпадает с обычной топологической замкнутостью (при стандартных предпосылках).
LaTeX
$$intrinsicClosure_{\\mathbb{k}}(s) = closure(s)$$
Lean4
@[simp]
theorem intrinsicClosure_eq_closure : intrinsicClosure 𝕜 s = closure s :=
by
ext x
simp only [mem_closure_iff, mem_intrinsicClosure]
refine ⟨?_, fun h => ⟨⟨x, _⟩, ?_, Subtype.coe_mk _ ?_⟩⟩
· rintro ⟨x, h, rfl⟩ t ht hx
obtain ⟨z, hz₁, hz₂⟩ := h _ (continuous_induced_dom.isOpen_preimage t ht) hx
exact ⟨z, hz₁, hz₂⟩
· rintro _ ⟨t, ht, rfl⟩ hx
obtain ⟨y, hyt, hys⟩ := h _ ht hx
exact ⟨⟨_, subset_affineSpan 𝕜 s hys⟩, hyt, hys⟩
· by_contra hc
obtain ⟨z, hz₁, hz₂⟩ := h _ (affineSpan 𝕜 s).closed_of_finiteDimensional.isOpen_compl hc
exact hz₁ (subset_affineSpan 𝕜 s hz₂)
