Commit 2023-09-11 18:53 d6303b84

View on Github →

feat: characterizations of monotonicity in locally finite orders (#6709)

depends on: #6711
depends on: #6712

Estimated changes

Modified Mathlib/Data/Finset/Interval.lean

added theorem Finset.antitone_iff'

added theorem Finset.antitone_iff

added theorem Finset.covby_cons

added theorem Finset.covby_iff'

added theorem Finset.covby_iff

added theorem Finset.covby_insert

added theorem Finset.monotone_iff'

added theorem Finset.monotone_iff

added theorem Finset.strictAnti_iff'

added theorem Finset.strictAnti_iff

added theorem Finset.strictMono_iff'

added theorem Finset.strictMono_iff

Modified Mathlib/Data/Finset/LocallyFinite.lean

added theorem antitone_iff_forall_covby

added theorem antitone_iff_forall_wcovby

added theorem le_iff_reflTransGen_covby

added theorem le_iff_transGen_wcovby

added theorem lt_iff_transGen_covby

added theorem monotone_iff_forall_covby

added theorem monotone_iff_forall_wcovby

added theorem strictAnti_iff_forall_covby

added theorem strictMono_iff_forall_covby

added theorem transGen_covby_of_lt

added theorem transGen_wcovby_of_le