to_locallyFinite — Mathlib

English

From a LocallyFinite.Realizer for F and f one obtains the local finiteness of f itself.

Русский

Из реализатора локально конечной структуры для F и f следует локальная конечность f.

LaTeX

$$$\operatorname{LocallyFinite}(f). $$$$

Lean4

theorem to_locallyFinite [TopologicalSpace α] {F : Ctop.Realizer α} {f : β → Set α} (R : LocallyFinite.Realizer F f) :
    LocallyFinite f := fun a ↦
  ⟨_, F.mem_nhds.2 ⟨(R.bas a).1, (R.bas a).2, Subset.rfl⟩,
    have := R.sets a;
    Set.toFinite _⟩

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