inter_biInter — 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 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]

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