biInter_inter — Mathlib

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 biInter_inter {ι α : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → Set α) (t : Set α) :
    ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t :=
  by
  haveI : Nonempty s := hs.to_subtype
  simp [biInter_eq_iInter, ← iInter_inter]

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