Commit 2020-06-28 21:26 3d72c970

View on Github →

chore(measure_theory/outer_measure,measure_space): use complete_lattice_of_Inf/Sup (#3185) Also add a few supporting lemmas about bsupr/binfi to order/complete_lattice

Estimated changes

Modified src/measure_theory/measure_space.lean

Modified src/measure_theory/outer_measure.lean

added theorem measure_theory.outer_measure.coe_supr

Modified src/order/complete_lattice.lean

modified theorem binfi_inf

added theorem binfi_le

added theorem binfi_le_binfi

added theorem bsupr_le

added theorem bsupr_le_bsupr

modified theorem infi_lt_iff

added theorem le_binfi

added theorem le_bsupr

modified theorem lt_supr_iff