isConstructible — Mathlib

English

Let X be a topological space and U be a subset of X. If U is open and retrocompact, then U is constructible.

Русский

Пусть X — топологическое пространство, а U — подмножество X. Тогда если U открытое и ретрокомпактное, то U является конструктируемым.

LaTeX

$$$\\forall X \\\\[TopologicalSpace X], \\\\forall U \\subseteq X, \\\\text{IsOpen}(U) \\\\land \\\\text{IsRetrocompact}(U) \\Rightarrow \\text{IsConstructible}(U).$$$

Lean4

theorem _root_.IsRetrocompact.isConstructible (hUopen : IsOpen U) (hUcomp : IsRetrocompact U) : IsConstructible U :=
  BooleanSubalgebra.subset_closure ⟨hUopen, hUcomp⟩

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