English
If s is nonempty, then ∩ i ∈ s (f i ∩ t) equals (∩ i ∈ s f i) ∩ t.
Русский
Пусть s ненулево, тогда ∩ i ∈ s (f i ∩ t) = (∩ i ∈ s f i) ∩ t.
LaTeX
$$$\\\\bigcap_{i \\in s} (f(i) \\cap t) = (\\\\bigcap_{i \\in s} f(i)) \\cap t$$$
Lean4
theorem inter_biInter {ι α : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → Set α) (t : Set α) :
⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i :=
by
rw [inter_comm, ← biInter_inter hs]
simp [inter_comm]