inter_iInter — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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