iInter_iInter_eq' — Mathlib

English

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

Русский

Пусть f: ι → α и g: α → Set β. Тогда пересечение по x и y с условием f(y)=x от g x равно пересечению по y: g(f y).

LaTeX

$$$\bigcap_{x} \bigcap_{y: f(y)=x} g(x) = \bigcap_{y} g(f(y))$$$

Lean4

@[simp]
theorem iInter_iInter_eq' {f : ι → α} {g : α → Set β} : ⋂ (x) (y) (_ : f y = x), g x = ⋂ y, g (f y) := by
  simpa using biInter_range

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