ShellFieldBorelMeasurableSpace

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

@[instance_reducible]

noncomputable def Algsuperdiff.Frozen.Assumptions.shellFieldBorelMeasurableSpace (d : ℕ) : MeasurableSpace (ShellField d)

The Borel measurable structure induced by the shell's compact-open topology.

Equations

• Algsuperdiff.Frozen.Assumptions.shellFieldBorelMeasurableSpace d = borel (Algsuperdiff.Frozen.Assumptions.ShellField d)