English
There is a criterion for when the preimage of a subset under the inclusion map is closed, expressed via an inclusion-related condition involving s and t.
Русский
Утверждается критерий замкнутости предобраза под множества через включение, выраженный через условия на s и t.
LaTeX
$$$\\forall s,t\\subseteq X:\\; \\text{IsClosed}(s\\downarrow\\cap t) \\iff s\\cap \\overline{(s\\cap t)} \\subseteq t.$$$
Lean4
theorem isClosed_preimage_val {s t : Set X} : IsClosed (s ↓∩ t) ↔ s ∩ closure (s ∩ t) ⊆ t :=
by
rw [← closure_eq_iff_isClosed, IsEmbedding.subtypeVal.closure_eq_preimage_closure_image, ←
Subtype.val_injective.image_injective.eq_iff, Subtype.image_preimage_coe, Subtype.image_preimage_coe,
subset_antisymm_iff, and_iff_left, Set.subset_inter_iff, and_iff_right]
exacts [Set.inter_subset_left, Set.subset_inter Set.inter_subset_left subset_closure]
