set_pi_mem_nhds — Mathlib

English

For a finite index set I, I.pi s ∈ nhds a if and only if ∀ i ∈ I, s i ∈ nhds(a i).

Русский

Для конечного множества индексов I: I.pi s ∈ nhds a тогда и только тогда, когда ∀ i ∈ I, s i ∈ nhds(a i).

LaTeX

$$$\\displaystyle I . Finite \\rightarrow (I.\\pi s \\in \\mathcal{N}(a) \\iff \\forall i \\in I, s(i) \\in \\mathcal{N}(a(i))).$$$

Lean4

theorem set_pi_mem_nhds {i : Set ι} {s : ∀ a, Set (A a)} {x : ∀ a, A a} (hi : i.Finite) (hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)) :
    pi i s ∈ 𝓝 x := by
  rw [pi_def, biInter_mem hi]
  exact fun a ha => (continuous_apply a).continuousAt (hs a ha)

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