English
A set-valued map f is locally finite iff there exists a LocallyFinite.Realizer F f over some ambient realizer F.
Русский
Множество отображений f локально конечно тогда и только тогда, когда существует LocallyFinite.Realizer F f над некоторым реализатором F.
LaTeX
$$$\operatorname{LocallyFinite}(f) \;\iff\; \operatorname{Nonempty}(\operatorname{LocallyFinite.Realizer} F f).$$$
Lean4
theorem locallyFinite_iff_exists_realizer [TopologicalSpace α] (F : Ctop.Realizer α) {f : β → Set α} :
LocallyFinite f ↔ Nonempty (LocallyFinite.Realizer F f) :=
⟨fun h ↦
let ⟨g, h₁⟩ := Classical.axiom_of_choice h
let ⟨g₂, h₂⟩ :=
Classical.axiom_of_choice fun x ↦
show ∃ b : F.σ, x ∈ F.F b ∧ F.F b ⊆ g x from
let ⟨h, _h'⟩ := h₁ x
F.mem_nhds.1 h
⟨⟨fun x ↦ ⟨g₂ x, (h₂ x).1⟩, fun x ↦
Finite.fintype <|
let ⟨_h, h'⟩ := h₁ x
h'.subset fun _i hi ↦ hi.mono (inter_subset_inter_right _ (h₂ x).2)⟩⟩,
fun ⟨R⟩ ↦ R.to_locallyFinite⟩
