biUnion_image

Mathlib.Data.Set.Lattice.Image

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

English

Let s be a set of elements, f: γ → α, and g: α → Set β. Then ⋃ x ∈ f'' s, g x equals ⋃ y ∈ s, g(f y).

Русский

Пусть s — множество элементов, f: γ → α, g: α → Set β. Тогда ⋃ x ∈ f'' s, g x = ⋃ y ∈ s, g(f y).

LaTeX

$$$\bigcup_{x \in f''s} g(x) = \bigcup_{y \in s} g(f(y))$$$

Lean4

theorem biUnion_image : ⋃ x ∈ f '' s, g x = ⋃ y ∈ s, g (f y) :=
  iSup_image

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

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

Разделы

Аффилиация

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