English
Let X be a topological space and f be a family of subsets of X indexed by the option-type on ι. Then the family is locally finite if and only if the subfamily indexed by Some i (i.e., by ι) is locally finite. Equivalently, a locally finite family indexed by Option ι remains locally finite after identifying ι with the image i ↦ Some i.
Русский
Пусть X – топологическое пространство и f – семейство подмножеств X, индексируемое по типу Option ι. Тогда это семейство локально конечное тогда и только тогда, когда подсемейство, индексируемое элементами Some i (то есть ι), локально конечное. Эквивалентно: локальная конечность сохраняется под перес indexing через внедрение i ↦ Some i.
LaTeX
$$$\\operatorname{LocallyFinite}(f) \\iff \\operatorname{LocallyFinite}(f \\circ \\mathrm{some})$$$
Lean4
theorem locallyFinite_option {f : Option ι → Set X} : LocallyFinite f ↔ LocallyFinite (f ∘ some) :=
by
rw [← (Equiv.optionEquivSumPUnit.{0, _} ι).symm.locallyFinite_comp_iff, locallyFinite_sum]
simp only [locallyFinite_of_finite, and_true]
rfl
