iInter_inter — Mathlib

English

Let ι be a nonempty index set and s ⊆ β, t_i ⊆ β for each i ∈ ι. Then (⋂_{i} t_i) ∩ s = ⋂_{i} (t_i ∩ s).

Русский

Пусть ι непустое множество индексов, и пусть t_i ⊆ β, s ⊆ β для каждого i. Тогда (⋂_{i} t_i) ∩ s = ⋂_{i} (t_i ∩ s).

LaTeX

$$$ (\bigcap_i t_i) \cap s = \bigcap_i (t_i \cap s) $$$

Lean4

theorem iInter_inter [Nonempty ι] (s : Set β) (t : ι → Set β) : (⋂ i, t i) ∩ s = ⋂ i, t i ∩ s :=
  iInf_inf

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