range_casesOn

Mathlib.Data.Nat.Set

URI: https://scilib.ai/kg/mathlib#Nat.range_casesOn

← MathLib Explorer

English

The range of Nat.casesOn n x f equals {x} ∪ range f.

Русский

Диапазон Nat.casesOn n x f равен {x} ∪ range f.

LaTeX

$$$ \\mathrm{range}(fun n => \\mathrm{Nat}.casesOn n x f) = \\{ x \\} \\cup \\mathrm{range} f$$$

Lean4

theorem range_casesOn {α : Type*} (x : α) (f : ℕ → α) :
    (Set.range fun n => Nat.casesOn n x f : Set α) = { x } ∪ Set.range f :=
  (range_of_succ _).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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