Measurable equivalences

This file extends the theory of measurable equivalences, providing utilities for working with products and unit types.

Main declarations

• MeasurableEquiv.punit: measurable equivalence between PUnits.

@[reducible, inline]

abbrev MeasurableEquiv.punit : PUnit.{x + 1} ≃ᵐ PUnit.{y + 1}

The measurable equivalence between two PUnits.

Equations

• MeasurableEquiv.punit = MeasurableEquiv.ofUniqueOfUnique PUnit.{?u.2 + 1} PUnit.{?u.1 + 1}