closure_union — Mathlib

English

Let X be a topological space and s, t be subsets of X. Then the closure distributes over union: cl(s ∪ t) = cl(s) ∪ cl(t).

Русский

Пусть X — топологическое пространство, и s, t — подмножества X. Замыкание распределяется по объединению: cl(s ∪ t) = cl(s) ∪ cl(t).

LaTeX

$$$\\\\overline{s \\\\\\cup t} = \\\\overline{s} \\\\cup \\\\overline{t}$$$

Lean4

@[simp]
theorem closure_union : closure (s ∪ t) = closure s ∪ closure t := by
  simp [closure_eq_compl_interior_compl, compl_inter]

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