Realizer — Mathlib

English

An instance asserting the existence of a LocallyFinite.Realizer for finite index sets.

Русский

Экземпляр, утверждающий существование LocallyFinite.Realizer при конечном индексе.

LaTeX

$$$\text{[Finite } \beta\text{]} \Rightarrow \operatorname{Nonempty}(\operatorname{LocallyFinite.Realizer} F f).$$$

Lean4

/-- A `Compact.Realizer s` is a realization that `s` is compact, namely it is a
choice of finite open covers for each set family covering `s`. -/
def Realizer [TopologicalSpace α] (s : Set α) :=
  ∀ {f : Filter α} (F : f.Realizer) (x : F.σ), f ≠ ⊥ → F.F x ⊆ s → { a // a ∈ s ∧ 𝓝 a ⊓ f ≠ ⊥ }

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