Commit 2023-07-21 10:06 995893e5

View on Github →

feat: minimals/maximals API (#5911) This PR adds some API to Data.Order.Minimal, with a few rewrite lemmas for membership in sets of maximals/minimals, lemmas that give sufficient conditions for two sets having the same maximal/minimal elements, and a bunch of lemmas about images/preimages of sets of maximal elements.

Estimated changes

Modified Mathlib/Order/Minimal.lean

added theorem RelEmbedding.inter_preimage_maximals_eq

added theorem RelEmbedding.inter_preimage_maximals_eq_of_subset

added theorem RelEmbedding.inter_preimage_minimals_eq

added theorem RelEmbedding.inter_preimage_minimals_eq_of_subset

added theorem RelEmbedding.maximals_image_eq

added theorem RelEmbedding.maximals_preimage_eq

added theorem RelEmbedding.minimals_image_eq

added theorem RelEmbedding.minimals_preimage_eq

added theorem inter_maximals_preimage_inter_eq_of_rel_iff_rel_on

added theorem inter_minimals_preimage_inter_eq_of_rel_iff_rel_on

added theorem inter_preimage_maximals_eq_of_rel_iff_rel_on_of_subset

added theorem inter_preimage_minimals_eq_of_rel_iff_rel_on_of_subset

added theorem maximals_Icc

added theorem maximals_Iic

added theorem maximals_Ioc

added theorem maximals_eq_maximals_of_subset_of_forall

added theorem maximals_image_of_rel_iff_rel_on

added theorem mem_maximals_iff

added theorem mem_maximals_iff_forall_lt_not_mem'

added theorem mem_maximals_iff_forall_lt_not_mem

added theorem mem_maximals_iff_forall_ssubset_not_mem

added theorem mem_maximals_setOf_iff

added theorem mem_minimals_iff

added theorem mem_minimals_iff_forall_lt_not_mem'

added theorem mem_minimals_iff_forall_lt_not_mem

added theorem mem_minimals_iff_forall_ssubset_not_mem

added theorem mem_minimals_setOf_iff

added theorem minimals_Icc

added theorem minimals_Ici

added theorem minimals_Ico

added theorem minimals_eq_minimals_of_subset_of_forall

added theorem minimals_image_of_rel_iff_rel