iInter_option — Mathlib

English

For a family s(o) indexed by an Option type, the intersection over all o equals s none ∩ ⋂_{i} s (some i).

Русский

Для семейства s(o) индексированного по Option, пересечение по всем o равно s none ∩ ⋂_{i} s (some i).

LaTeX

$$$ \bigcap_o s(o) = s(\text{none}) \cap \bigcap_i s(\text{some}(i)) $$$

Lean4

theorem iInter_option {ι} (s : Option ι → Set α) : ⋂ o, s o = s none ∩ ⋂ i, s (some i) :=
  iInf_option s

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