Commit 2023-07-21 04:29 af306e0a

View on Github →

feat: basic measure / topology lemmas (#5986)

Estimated changes

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.nonempty_compl_of_nontrivial

Modified Mathlib/MeasureTheory/Measure/OpenPos.lean

added theorem MeasureTheory.Measure.measure_ne_zero

added theorem Metric.measure_closedBall_pos_iff

Modified Mathlib/Topology/Separation.lean