IsLocallyConstructible — Mathlib

English

A set is locally constructible if around every point there exists a neighborhood where the intersection with the set is constructible.

Русский

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

LaTeX

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

Lean4

/-- A set in a topological space is locally constructible, if every point has a neighborhood on
which the set is constructible. -/
@[stacks 005G]
def IsLocallyConstructible (s : Set X) : Prop :=
  ∀ x, ∃ U ∈ 𝓝 x, IsOpen U ∧ IsConstructible (U ↓∩ s)

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