isUpperSet_iInter₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isUpperSet_iInter₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsUpperSet (f i j)) : IsUpperSet (⋂ (i) (j), f i j) :=
  isUpperSet_iInter fun i => isUpperSet_iInter <| hf i

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