countable_range

Mathlib.Data.Set.Countable

URI: https://scilib.ai/kg/mathlib#Set.countable_range

English

If ι is countable and f: ι → β, then range f is countable.

Русский

Если множество индексов ι счётно и функция f : ι → β задана, то диапазон f счётен.

LaTeX

$$$[\text{Countable } ι] \Rightarrow (\mathrm{range}(f)).Countable$$$

Lean4

theorem countable_range [Countable ι] (f : ι → β) : (range f).Countable :=
  rangeFactorization_surjective.countable.to_set

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

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

Разделы

Аффилиация

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