Topology and Borel structure on locally finite trees

Offspring is a countable product of discrete copies of ℕ, hence Polish, and the canonical fields form a closed subset. The topology is the subtype topology: a sequence of trees converges exactly when every offspring coordinate is eventually constant. This is the Polish structure of Freezing1/PlaneTree.lean, from which isClosed_canonical and the continuity lemmas are adapted.

The only instance declared in this file is PolishSpace Tree. The measurable structure is Mathlib's subtype σ-algebra, induced by the product σ-algebra of Offspring; Mathlib's Subtype.borelSpace and Pi.borelSpace already make it the Borel σ-algebra of the topology. No instance is installed on Address = List ℕ: the product σ-algebra only involves the measurable space on the values.

theorem BGW.LocallyFinite.isClosed_canonical : IsClosed {f : Offspring | Canonical f}

instance BGW.LocallyFinite.instPolishSpaceTree : PolishSpace Tree

theorem BGW.LocallyFinite.continuous_offspring (u : Address) : Continuous fun (T : Tree) => ↑T u

theorem BGW.LocallyFinite.continuous_degree : Continuous degree

theorem BGW.LocallyFinite.continuous_child (j : ℕ) : Continuous fun (T : Tree) => child T j