isUpperSet_iUnion — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isUpperSet_iUnion {f : ι → Set α} (hf : ∀ i, IsUpperSet (f i)) : IsUpperSet (⋃ i, f i) :=
  isUpperSet_sUnion <| forall_mem_range.2 hf

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