disjoint_closure_of_disjoint_isOpen

English

In an extremally disconnected space, the closures of two disjoint open sets are disjoint.

Русский

В экстремально разобщимом пространстве замыкания двух непересекающихся открытых множеств также не пересекаются.

LaTeX

$$$$ \\text{If } U_1, U_2 \\text{ are disjoint open, then } \\overline{U_1} \\cap \\overline{U_2} = \\emptyset. $$$$

Lean4

/-- Lemma 2.2 in [Gleason, *Projective topological spaces*][gleason1958]:
in an extremally disconnected space, if $U_1$ and $U_2$ are disjoint open sets,
then $\overline{U_1}$ and $\overline{U_2}$ are also disjoint. -/
theorem disjoint_closure_of_disjoint_isOpen [ExtremallyDisconnected A] {U₁ U₂ : Set A} (h : Disjoint U₁ U₂)
    (hU₁ : IsOpen U₁) (hU₂ : IsOpen U₂) : Disjoint (closure U₁) (closure U₂) :=
  (h.closure_right hU₁).closure_left <| open_closure U₂ hU₂

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