locallyFinite_of_finite

Mathlib.Topology.LocallyFinite

URI: https://scilib.ai/kg/mathlib#locallyFinite_of_finite

English

If the index set ι is finite, then any family f: ι → Set X is locally finite.

Русский

Если множество индексов ι конечно, то любая семейство f: ι → Set X локально конечно.

LaTeX

$$$\\text{LocallyFinite}(f)$ for finite ι$$

Lean4

theorem locallyFinite_of_finite [Finite ι] (f : ι → Set X) : LocallyFinite f := fun _ => ⟨univ, univ_mem, toFinite _⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru