biInter_range

Mathlib.Data.Set.Lattice.Image

URI: https://scilib.ai/kg/mathlib#Set.biInter_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

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

Lean4

theorem biInter_range {f : ι → α} {g : α → Set β} : ⋂ x ∈ range f, g x = ⋂ y, g (f y) :=
  iInf_range

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

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

Разделы

Аффилиация

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