English
If the whole space is covered by two disjoint open sets a and b, then a is clopen.
Русский
Если всякое пространство покрыто двумя попарно непересекающимися открытыми множествами a и b, то a является клиopen.
LaTeX
$$$$ \operatorname{IsClopen}(a) $$$$
Lean4
/-- The intersection of a disjoint covering by two open sets of a clopen set will be clopen. -/
theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s) (cover : s ⊆ a ∪ b) (ha : IsOpen a)
(hb : IsOpen b) (hab : Disjoint a b) : IsClopen (s ∩ a) :=
by
refine ⟨?_, IsOpen.inter h.2 ha⟩
have : IsClosed (s ∩ bᶜ) := IsClosed.inter h.1 (isClosed_compl_iff.2 hb)
convert this using 1
refine (inter_subset_inter_right s hab.subset_compl_right).antisymm ?_
rintro x ⟨hx₁, hx₂⟩
exact ⟨hx₁, by simpa [notMem_of_mem_compl hx₂] using cover hx₁⟩
