set_pi_mem_nhds_iff — Mathlib

English

A variant of the previous equivalence tailored to an abstract setting for pi spaces.

Русский

Вариант предыдущего эквивалентного условия для абстрактного окружения Pi-пространств.

LaTeX

$$$\\displaystyle \\text{set\_pi\_mem\_nhds\_iff'} \\approx \\text{(equivalent formulation for finite pi-neighborhoods)}$$$

Lean4

theorem set_pi_mem_nhds_iff {I : Set ι} (hI : I.Finite) {s : ∀ i, Set (A i)} (a : ∀ i, A i) :
    I.pi s ∈ 𝓝 a ↔ ∀ i : ι, i ∈ I → s i ∈ 𝓝 (a i) := by rw [nhds_pi, pi_mem_pi_iff hI]

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