biUnion_range

Mathlib.Data.Set.Lattice.Image

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

English

Let f: ι → α and g: α → Set β. Then ∪_{x ∈ range f} g(x) = ∪_{y} g(f(y)).

Русский

Пусть f: ι → α и g: α → Set β. Тогда объединение по x ∈ range f равно объединению по y: g(f(y)).

LaTeX

$$$\bigcup_{x \in \operatorname{range}(f)} g(x) = \bigcup_{y} g(f(y))$$$

Lean4

theorem biUnion_range {f : ι → α} {g : α → Set β} : ⋃ x ∈ range f, g x = ⋃ y, g (f y) :=
  iSup_range

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

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

Разделы

Аффилиация

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