mem_nhds_of_pi_mem_nhds — Mathlib

English

If I ⊂ ι is finite and each s(a) ∈ nhds(x(a)) for a ∈ I, then I.pi s ∈ nhds x.

Русский

Если I конечно и для каждого a ∈ I выполняется s(a) ∈ nhds(x(a)), то I.pi s ∈ nhds x.

LaTeX

$$$\\displaystyle I \\text{ finite } \\to ( \\forall a \\in I, s(a) \\in \\mathcal{N}(x(a)) ) \\Rightarrow \\pi I s \\in \\mathcal{N}(x).$$$

Lean4

theorem mem_nhds_of_pi_mem_nhds {I : Set ι} {s : ∀ i, Set (A i)} (a : ∀ i, A i) (hs : I.pi s ∈ 𝓝 a) {i : ι}
    (hi : i ∈ I) : s i ∈ 𝓝 (a i) := by rw [nhds_pi] at hs; exact mem_of_pi_mem_pi hs hi

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