isLowerSet_iInter — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isLowerSet_iInter {f : ι → Set α} (hf : ∀ i, IsLowerSet (f i)) : IsLowerSet (⋂ i, f i) :=
  isLowerSet_sInter <| forall_mem_range.2 hf

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