union — Mathlib

English

If s and t are compact, then their union s ∪ t is compact.

Русский

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

LaTeX

$$$\operatorname{IsCompact}(s) \land \operatorname{IsCompact}(t) \Rightarrow \operatorname{IsCompact}(s \cup t)$$$

Lean4

theorem union (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∪ t) := by rw [union_eq_iUnion];
  exact isCompact_iUnion fun b => by cases b <;> assumption

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