isOpen_biInter — Mathlib

English

If s is finite and each i ∈ s, IsOpen(f(i)), then ⋂ i ∈ s, f(i) is open.

Русский

Если s конечно и каждый i∈s, IsOpen(f(i)), тогда ⋂ i∈s f(i) открыто.

LaTeX

$$$s.Finite \rightarrow (\forall i \in s, IsOpen (f i)) \rightarrow IsOpen (\bigcap_{i \in s} f i)$$$

Lean4

theorem isOpen_biInter {s : Set α} {f : α → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsOpen (f i)) :
    IsOpen (⋂ i ∈ s, f i) :=
  sInter_image f s ▸ (hs.image _).isOpen_sInter (forall_mem_image.2 h)

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