isOpen_iInter₂ — Mathlib

English

The two-index intersection of a collection of open sets is open: if f i j is open for all i and j, then ⋂i,⋂j f(i,j) is open.

Русский

Двухиндексное пересечение множества открытых множеств открыто.

LaTeX

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

Lean4

theorem isOpen_iInter₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsOpen (f i j)) : IsOpen (⋂ i, ⋂ j, f i j) :=
  isOpen_iInter fun _ ↦ isOpen_iInter <| hf _

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