exists_finset_piecewise_mem_of_mem_nhds

English

The Pi-topology equals the generateFrom topology generated by basic pi-sets.

Русский

Топология Pi равна generateFrom, порождаемой базой множеств pi.

LaTeX

$$$\\displaystyle \\Pi\\text{topologicalSpace} = \\operatorname{generateFrom}\\{ g \\mid \\exists s,i, (\\forall a \\in i, s(a) \\text{ открыто}) \\land g = \\pi(i,s) \\}$$$

Lean4

theorem exists_finset_piecewise_mem_of_mem_nhds [DecidableEq ι] {s : Set (∀ a, A a)} {x : ∀ a, A a} (hs : s ∈ 𝓝 x)
    (y : ∀ a, A a) : ∃ I : Finset ι, I.piecewise x y ∈ s :=
  by
  simp only [nhds_pi, Filter.mem_pi'] at hs
  rcases hs with ⟨I, t, htx, hts⟩
  refine ⟨I, hts fun i hi => ?_⟩
  simpa [Finset.mem_coe.1 hi] using mem_of_mem_nhds (htx i)

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