instNonemptyRealizerOfFinite — Mathlib

English

If β is finite, then for any F and f, there exists a LocallyFinite.Realizer F f.

Русский

При конечности β существует LocallyFinite.Realizer F f для любых F и f.

LaTeX

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

Lean4

instance [TopologicalSpace α] [Finite β] (F : Ctop.Realizer α) (f : β → Set α) :
    Nonempty (LocallyFinite.Realizer F f) :=
  (locallyFinite_iff_exists_realizer _).1 <| locallyFinite_of_finite _

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