English
If u is open and v is disjoint from the frontier of u, then the preimage of u under the inclusion map is clopen.
Русский
Если u открыто и v распознанно дизъюнктивно к границе u, то предобраз u по включению непрерывной карты является открытым и закрытым.
LaTeX
$$$\text{IsClopen}(\,v\downarrow\cap u\,)$$$
Lean4
theorem isClopen_preimage_val {X : Type*} [TopologicalSpace X] {u v : Set X} (hu : IsOpen u)
(huv : Disjoint (frontier u) v) : IsClopen (v ↓∩ u) :=
by
refine ⟨?_, isOpen_induced hu (f := Subtype.val)⟩
refine isClosed_induced_iff.mpr ⟨closure u, isClosed_closure, ?_⟩
apply image_val_injective
simp only [Subtype.image_preimage_coe]
rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_comm _ (frontier u), huv.inter_eq, union_empty]
