pi_generateFrom_eq — Mathlib

English

If nhds x contains s, then there exists a finite index set I and a piecewise construction x,y so that the piecewise element lies in s.

Русский

Если nhds x содержит s, существует конечный набор индексов I и разбиение piecewise x y ∈ s.

LaTeX

$$$\\displaystyle \\exists I : \\mathrm{Finset}\\ ι, I.piecewise x y \\in s$$$

Lean4

theorem pi_generateFrom_eq {A : ι → Type*} {g : ∀ a, Set (Set (A a))} :
    (@Pi.topologicalSpace ι A fun a => generateFrom (g a)) =
      generateFrom {t | ∃ (s : ∀ a, Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = pi (↑i) s} :=
  by
  refine le_antisymm ?_ ?_
  · apply le_generateFrom
    rintro _ ⟨s, i, hi, rfl⟩
    letI := fun a => generateFrom (g a)
    exact isOpen_set_pi i.finite_toSet (fun a ha => GenerateOpen.basic _ (hi a ha))
  ·
    classical
    refine le_iInf fun i => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_
    refine GenerateOpen.basic _ ⟨update (fun i => univ) i s, { i }, ?_⟩
    simp [hs]

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