inter_of_isOpen — Mathlib

English

In a quasi-separated space, the intersection of two open compact sets is compact.

Русский

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

LaTeX

$$IsCompact U ∧ IsOpen U ∧ IsCompact V ∧ IsOpen V ⇒ IsCompact (U ∩ V)$$

Lean4

theorem inter_of_isOpen (hUcomp : IsCompact U) (hVcomp : IsCompact V) (hUopen : IsOpen U) (hVopen : IsOpen V) :
    IsCompact (U ∩ V) :=
  QuasiSeparatedSpace.inter_isCompact _ _ hUopen hUcomp hVopen hVcomp

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