Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measure_theory.content.inner_content_mono'

Modification history

2022-04-04 23:36

src/measure_theory/measure/content.lean

chore(order/complete_lattice): Generalize `⨆`/`⨅` lemmas to dependent families (#13154) …

Modified measure_theory.content.inner_content_mono'View on Github →

2021-05-16 18:58

src/measure_theory/content.lean

refactor(measure_theory/haar_measure): move general material to content.lean, make content a structure (#7615) …

Added measure_theory.content.inner_content_mono'View on Github →