isOpen_forall_mem — Mathlib

English

For any open A_i, the open set {f : Πʳ i, [R i, A i] | ∀ i, p i → f i ∈ A_i} is open.

Русский

Для любых открытых A_i множество {f | ∀ i, p i → f i ∈ A_i} открыто.

LaTeX

$$$\\text{IsOpen}\\{f : Πʳ i, [R i, A i] | ∀ i, p i → \\text{mem}(A_i, f.i)\\}$$$

Lean4

theorem isOpen_forall_mem : IsOpen {f : Πʳ i, [R i, A i] | ∀ i, f.1 i ∈ A i} :=
  by
  simp_rw [topologicalSpace_eq_iSup cofinite, isOpen_iSup_iff, isOpen_coinduced]
  exact fun S hS ↦ isOpen_forall_mem_of_principal hAopen hS

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