union — Mathlib

English

If s and t are retrocompact then their union is retrocompact.

Русский

Если s и t ретрокомпактны, то их объединение retrocompact.

LaTeX

$$$\text{IsRetrocompact}(s) \land \text{IsRetrocompact}(t) \Rightarrow \text{IsRetrocompact}(s \cup t)$$$

Lean4

theorem union (hs : IsRetrocompact s) (ht : IsRetrocompact t) : IsRetrocompact (s ∪ t : Set X) := fun _U hUcomp hUopen ↦
  union_inter_distrib_right .. ▸ (hs hUcomp hUopen).union (ht hUcomp hUopen)

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