isLowerSet_iInter₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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