inter — Mathlib

English

In a Hausdorff space, the intersection of two compact sets is compact.

Русский

В Хаусдорфовом пространстве пересечение двух компактных множеств компактно.

LaTeX

$$$[T2Space X] {s,t\\subset X}\\; IsCompact s \\land IsCompact t \\Rightarrow IsCompact (s\\cap t).$$$

Lean4

theorem inter [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∩ t) :=
  hs.inter_right <| ht.isClosed

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