iUnion_image_left

Mathlib.Data.Set.Lattice.Image

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

English

The left side of a lemma expresses the iUnion over a family of images equals the image2 of the function over a pair of indexed sets.

Русский

Левая часть леммы выражает iUnion над образом как image2 над парой индексов.

LaTeX

$$$\bigcup_{a \in s} f(a)'' t = \mathrm{image2}(f,s,t)$$$

Lean4

theorem iUnion_image_left : ⋃ a ∈ s, f a '' t = image2 f s t := by simp only [image2_eq_iUnion, image_eq_iUnion]

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

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

Разделы

Аффилиация

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