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