subset_closure_inter_union_closure_compl_left

English

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

Русский

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

LaTeX

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

Lean4

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

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