Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measurable.inf_const

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 measurable.inf_constView on Github →