isRetrocompact_iff_isCompact — Mathlib

English

A set is locally constructible if every point has a neighborhood on which the set is constructible.

Русский

Множество локально конструируемое, если вокруг каждой точки существует окрестность, где множество конструируемо.

LaTeX

$$$IsLocallyConstructible(s) := \\forall x, \\exists U \\in 𝓝(x), IsOpen(U) \\land IsConstructible(U \\cap s).$$$

Lean4

@[stacks 0069 "Iff form of (2). Note that Stacks doesn't define quasi-separated spaces."]
theorem _root_.QuasiSeparatedSpace.isRetrocompact_iff_isCompact (hU : IsOpen U) : IsRetrocompact U ↔ IsCompact U :=
  ⟨IsRetrocompact.isCompact, (IsCompact.isRetrocompact · hU)⟩

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