subset_closure_inter_union_closure_compl_right

English

For any sets s,t in a topological space X, the closure of s is contained in the closure of s ∩ t together with the closure of tᶜ: closure s ⊆ closure(s ∩ t) ∪ closure(tᶜ).

Русский

Для любых множеств s,t в топологическом пространстве X замыкание s ⊆ замыкание( s ∩ t ) ∪ замыкание( tᶜ ).

LaTeX

$$$\\\\overline{s} \\\\subseteq \\\\overline{s \\\\\\cap t} \\\\cup \\\\overline{t^c}$$$

Lean4

theorem subset_closure_inter_union_closure_compl_right : closure s ⊆ closure (s ∩ t) ∪ closure tᶜ :=
  (closure_mono <| subset_inter_union_compl_right ..).trans_eq closure_union

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