iUnion_singleton_eq_range

Mathlib.Data.Set.Lattice

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

English

Let f: α → β. The union over x in α of the singleton {f(x)} equals the range of f.

Русский

Пусть f: α → β. Объединение по x из α одномерной величины {f(x)} равно образу f.

LaTeX

$$$$ \\bigcup_{x \\in \\alpha} \\{ f(x) \\} = \\operatorname{range} f. $$$$

Lean4

@[simp]
theorem iUnion_singleton_eq_range (f : α → β) : ⋃ x : α, {f x} = range f :=
  by
  ext x
  simp [@eq_comm _ x]

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

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

Разделы

Аффилиация

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