Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ae_measurable.const_inf

Modification history

2021-12-07 18:28
src/measure_theory/lattice.lean
feat(measure_theory/lattice): define typeclasses for measurability of lattice operations, define a lattice on ae_eq_fun (#10591) …
Added ae_measurable.const_infView on Github →