isUpperSet_iInter — Mathlib

English

The intersection over i of upper sets is upper: if f(i) is upper for all i, then ⋂ i f(i) is upper.

Русский

Пересечение по i верхних множеств верхнее: если для всех i f(i) верхнее, то ⋂ i f(i) верхнее.

LaTeX

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

Lean4

theorem isUpperSet_iInter {f : ι → Set α} (hf : ∀ i, IsUpperSet (f i)) : IsUpperSet (⋂ i, f i) :=
  isUpperSet_sInter <| forall_mem_range.2 hf

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