English
Pi.topologicalSpace equals the generateFrom construction built from sets described by pi on finite subsets.
Русский
Pi.topologicalSpace равно конструктору generateFrom, описанному через pi на конечных подмножеств.
LaTeX
$$$\\displaystyle \\Pi.topologicalSpace = \\operatorname{generateFrom}\\{ g \\mid \\exists s,i, (\\forall a \\in i, IsOpen(s(a)) ) \\land g = \\pi(i,s) \\}$$$
Lean4
theorem pi_eq_generateFrom :
Pi.topologicalSpace =
generateFrom {g | ∃ (s : ∀ a, Set (A a)) (i : Finset ι), (∀ a ∈ i, IsOpen (s a)) ∧ g = pi (↑i) s} :=
calc
Pi.topologicalSpace
_ = @Pi.topologicalSpace ι A fun _ => generateFrom {s | IsOpen s} := by simp only [generateFrom_setOf_isOpen]
_ = _ := pi_generateFrom_eq
