isLowerSet_iUnion — Mathlib

English

If f(i) is lower for each i, then the union over i is lower: ⋃ i f(i) is a lower set.

Русский

Если каждый f(i) является нижним множеством, то объединение по i — нижнее множество.

LaTeX

$$$\forall i, IsLowerSet(f(i)) \Rightarrow IsLowerSet(\bigcup_i f(i))$$$

Lean4

theorem isLowerSet_iUnion {f : ι → Set α} (hf : ∀ i, IsLowerSet (f i)) : IsLowerSet (⋃ i, f i) :=
  isLowerSet_sUnion <| forall_mem_range.2 hf

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