Commit 2026-04-08 17:43 5dcb1568

View on Github →

chore(Order/Minimal): use to_dual (#37732)

Estimated changes

Modified Mathlib/Order/Minimal.lean

deleted theorem IsGreatest.maximal

deleted theorem IsGreatest.maximal_iff

deleted theorem Maximal.and_left

deleted theorem Maximal.and_right

deleted theorem Maximal.eq_of_ge

deleted theorem Maximal.eq_of_le

deleted theorem Maximal.le

deleted theorem Maximal.mono

deleted theorem Maximal.not_gt

deleted theorem Maximal.not_prop_of_gt

deleted theorem Maximal.or

deleted theorem MaximalFor.anti

deleted theorem MaximalFor.le

deleted theorem MaximalFor.maximal_of_strictMonoOn

deleted theorem MaximalFor.minimalFor_of_strictAntiOn_comp

deleted theorem MaximalFor.minimal_of_strictAntiOn

deleted theorem MaximalFor.not_gt

deleted theorem MaximalFor.not_prop_of_gt

deleted theorem MaximalFor.of_strictMonoOn_comp

deleted theorem OrderEmbedding.image_setOf_maximal

modified theorem OrderEmbedding.image_setOf_minimal

deleted theorem OrderEmbedding.inter_preimage_setOf_maximal_eq_of_subset

deleted theorem OrderEmbedding.maximal_apply_iff

deleted theorem OrderEmbedding.maximal_apply_mem_inter_range_iff

deleted theorem OrderEmbedding.maximal_mem_image

deleted theorem OrderEmbedding.maximal_mem_image_iff

deleted theorem OrderIso.image_setOf_maximal

deleted theorem OrderIso.map_maximal_mem

deleted def OrderIso.setOfMaximalIsoSetOfMinimal

deleted theorem Set.Subsingleton.maximal_mem_iff

deleted theorem exists_maximalFor_of_wellFoundedGT

deleted theorem exists_maximal_ge_of_wellFoundedGT

deleted theorem exists_maximal_of_wellFoundedGT

deleted theorem image_antitone_setOf_maximal

deleted theorem image_antitone_setOf_maximal_mem

deleted theorem image_monotone_setOf_maximal

deleted theorem image_monotone_setOf_maximal_mem

deleted theorem maximalFor_eq_iff

deleted theorem maximalFor_id

deleted theorem maximalFor_iff_forall_gt

deleted theorem maximal_and_iff_left_of_imp

deleted theorem maximal_and_iff_right_of_imp

deleted theorem maximal_eq_iff

deleted theorem maximal_false

deleted theorem maximal_ge_iff

deleted theorem maximal_gt_iff

deleted theorem maximal_iff

deleted theorem maximal_iff_eq

deleted theorem maximal_iff_forall_gt

deleted theorem maximal_iff_isMax

deleted theorem maximal_iff_maximal_of_imp_of_forall

deleted theorem maximal_le_iff

deleted theorem maximal_maximal

deleted theorem maximal_mem_Icc

deleted theorem maximal_mem_Ioc

deleted theorem maximal_mem_iff

deleted theorem maximal_mem_image_antitone

deleted theorem maximal_mem_image_antitone_iff

deleted theorem maximal_mem_image_monotone

deleted theorem maximal_mem_image_monotone_iff

deleted theorem maximal_subtype

deleted theorem maximal_toDual

deleted theorem maximal_true

deleted theorem maximal_true_subtype

modified theorem minimalFor_eq_iff

modified theorem minimalFor_id

modified theorem minimal_eq_iff

modified theorem minimal_false

modified theorem minimal_ge_iff

modified theorem minimal_le_iff

modified theorem minimal_lt_iff

modified theorem minimal_minimal

modified theorem minimal_subtype

modified theorem minimal_toDual

modified theorem minimal_true

deleted theorem not_maximal_iff

deleted theorem not_maximal_iff_exists_gt

deleted theorem setOf_maximal_subset