ProbNetKAT

Formalization of ProbNetKAT.

• Cantor
• Scott
• Measure extension

Main theorems and definitions

• ProbNetKAT.cantor_borel_eq_scott_borel: Connecting the Borel sets generated by the two topologies.