iUnion — Mathlib

English

Let f be a family of sets indexed by ι. If every f(i) is a RelLowerSet with respect to P, then the union over all i of f(i) is a RelLowerSet with respect to P.

Русский

Пусть дана семейство множеств f(i) ⊆ α индексированное i ∈ ι. Если для каждого i множество f(i) является RelLowerSet относительно P, то объединение ⋃_{i} f(i) также является RelLowerSet относительно P.

LaTeX

$$$\biggl(\forall i, IsRelLowerSet (f(i), P)\biggr) \Rightarrow IsRelLowerSet\Bigl(\bigcup_{i} f(i)\Bigr) P$$$

Lean4

protected theorem iUnion {f : ι → Set α} (hf : ∀ i, IsRelLowerSet (f i) P) : IsRelLowerSet (⋃ i, f i) P :=
  .sUnion (forall_mem_range.2 hf)

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