biInter_image

Mathlib.Data.Set.Lattice.Image

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

English

Let s be a set, f: γ → α, 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

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

Lean4

theorem biInter_image : ⋂ x ∈ f '' s, g x = ⋂ y ∈ s, g (f y) :=
  iInf_image

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

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

Разделы

Аффилиация

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