Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-12 05:02 f58f3404

View on Github →

feat(order/lattice): add monotone.le_map_sup and monotone.map_inf_le (#1673) Use it to simplify some proofs in data/rel.

Estimated changes

modified theorem rel.core_mono
added theorem rel.core_subset
modified theorem rel.core_union
modified theorem rel.image_mono
added theorem rel.image_subset
added theorem monotone.le_map_sup
added theorem monotone.map_inf_le