isConstructible — Mathlib

English

If X is a prespectral, quasi-separated and compact space, then every locally constructible subset is constructible.

Русский

Если X — пространcтво Prespectral и QuasiSeparated и компактно, то любая локально конструируемая подмножество является конструктируемым.

LaTeX

$$$\\operatorname{IsLocallyConstructible}(s) \\Rightarrow \\operatorname{IsConstructible}(s).$$$

Lean4

theorem isConstructible [PrespectralSpace X] [QuasiSeparatedSpace X] [CompactSpace X] (hs : IsLocallyConstructible s) :
    IsConstructible s :=
  hs.isConstructible_of_subset_of_isCompact s.subset_univ isCompact_univ

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