Commit 2023-10-31 18:07 43030491

View on Github →

feat: let push_neg replace not (Set.Nonempty s) with s = emptyset (#8000)

Estimated changes

Modified Counterexamples/Phillips.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/Analysis/Convex/StoneSeparation.lean

Modified Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Init/Set.lean

Modified Mathlib/MeasureTheory/Covering/Vitali.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Modified Mathlib/Tactic/PushNeg.lean

added theorem Mathlib.Tactic.PushNeg.empty_ne_eq_nonempty

added theorem Mathlib.Tactic.PushNeg.ne_empty_eq_nonempty

added theorem Mathlib.Tactic.PushNeg.not_nonempty_eq

Modified Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/Connected/Basic.lean

Modified Mathlib/Topology/ExtremallyDisconnected.lean

Modified test/push_neg.lean