isOpen_set_pi — Mathlib

English

If each s(a) is open and a finite index set i is used, then the Pi-set pi i s is open.

Русский

Если каждый s(a) открыто и индекс конечен, то множество пи i s открыто.

LaTeX

$$$\\displaystyle \\text{IsOpen}(\\pi i s).$$$

Lean4

theorem isOpen_set_pi {i : Set ι} {s : ∀ a, Set (A a)} (hi : i.Finite) (hs : ∀ a ∈ i, IsOpen (s a)) : IsOpen (pi i s) :=
  by rw [pi_def]; exact hi.isOpen_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)

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