isRetrocompact — Mathlib

English

If a set U is open and compact in a quasi-separated space, then U is retrocompact.

Русский

Если множество U открыто и компактно в квазиизолированном пространстве, то U ретрокомпактно.

LaTeX

$$$\\forall X\\ [TopologicalSpace X], \\forall U \\subseteq X, IsOpen(U) \\land IsCompact(U) \\Rightarrow IsRetrocompact(U).$$$

Lean4

theorem _root_.IsCompact.isRetrocompact (hU' : IsCompact U) (hU : IsOpen U) : IsRetrocompact U := fun _ hV' hV ↦
  hU'.inter_of_isOpen hV' hU hV

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