iInter — Mathlib

English

If Nonempty index type ι and every f i satisfies IsRelLowerSet (f i) P, then the intersection over i of f i is RelLowerSet with respect to P.

Русский

Пусть ι непусто и каждому i из ι удовлетворяет IsRelLowerSet (f i) P. Тогда пересечение ⋂ i f i является RelLowerSet относительно P.

LaTeX

$$$[Nonempty \ ι] \{f : ι \to Set α\} (\forall i, IsRelLowerSet (f i) P) : IsRelLowerSet (\bigcap_{i} f i) P$$$

Lean4

protected theorem iInter [Nonempty ι] {f : ι → Set α} (hf : ∀ i, IsRelLowerSet (f i) P) : IsRelLowerSet (⋂ i, f i) P :=
  .sInter (range_nonempty f) (forall_mem_range.2 hf)

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