English
Let p be a predicate on α and s a family of subsets s(x) ⊆ β indexed by x in the subtype {x | p(x)}. Then the intersection of all s(x) over x in the subtype equals the intersection over all x with p(x) of s(⟨x, hx⟩).
Русский
Пусть p — предикат на α и семейство множеств s(x) ⊆ β индексированы по подтипу {x | p(x)}. Тогда пересечение всех s(x) по x в подтипе равно пересечению по всем x с p(x) множества s(⟨x, hx⟩).
LaTeX
$$$\\\\bigcap_{x : \\\\{ x \\\\mid p(x) \\\}} s(x) \\\\;=\\\\; \\\\bigcap_{x} \\\\bigcap_{h \\\\in p(x)} s(\\\\langle x, h \\\\rangle) $$$
Lean4
theorem iInter_subtype (p : α → Prop) (s : { x // p x } → Set β) :
⋂ x : { x // p x }, s x = ⋂ (x) (hx : p x), s ⟨x, hx⟩ :=
iInf_subtype
