Commit 2023-07-20 06:11 02f74960

View on Github →

chore: gcongr attributes for sup/inf, min/max, union/intersection/complement, image/preimage (#6016)

Estimated changes

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.compl_subset_compl_of_subset

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.iInter_mono''

added theorem Set.iUnion_mono''

deleted theorem Set.sUnion_mono

Modified Mathlib/Order/CompleteLattice.lean

Modified Mathlib/Order/Heyting/Basic.lean

Modified Mathlib/Order/Lattice.lean

Modified Mathlib/Order/MinMax.lean

added theorem max_le_max_left

added theorem max_le_max_right

added theorem min_le_min_left

added theorem min_le_min_right