English
Let p : ι → Prop, q : ι → ι' → Prop, and s : ∀ x y, p x ∧ q x y → Set α. Then the intersection over x, y, h of s x y h equals the intersection over x, hx ∈ p x and y, hy ∈ q x y of s x y ⟨hx, hy⟩.
Русский
Пусть p : ι → Prop, q : ι → ι' → Prop и s : ∀ x y, p x ∧ q x y → Set α. Тогда пересечение по x, y и h множеств s(x,y,h) равно пересечению по x, hx ∈ p x и y, hy ∈ q x y соответственно s(x,y,⟨hx,hy⟩).
LaTeX
$$$$\\bigcap_{x:\\iota} \\bigcap_{y:\\iota'} \\bigcap_{h: p(x) \\land q(x,y)} s(x,y,h) = \\bigcap_{x:\\iota} \\bigcap_{hx: p(x)} \\bigcap_{y:\\iota'} \\bigcap_{hy: q(x,y)} s(x,y,\\langle hx, hy\\rangle).$$$$
Lean4
@[simp]
theorem biInter_and (p : ι → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p x ∧ q x y → Set α) :
⋂ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h = ⋂ (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y ⟨hx, hy⟩ := by
simp only [iInter_and, @iInter_comm _ ι']
