Commit 2024-10-01 22:56 f1843eb9

View on Github →

chore(Data/Finset): split lattice file (#17049) The file Data/Finset/Lattice contained two disjoint developments, with disjoint imports, forming one natural cut location. We also split max and min into a separate file.

Estimated changes

deleted theorem Finset.coe_max'
deleted theorem Finset.coe_min'
deleted theorem Finset.exists_max_image
deleted theorem Finset.exists_min_image
deleted theorem Finset.exists_next_left
deleted theorem Finset.exists_next_right
deleted theorem Finset.iInf_biUnion
deleted theorem Finset.iInf_coe
deleted theorem Finset.iInf_finset_image
deleted theorem Finset.iInf_insert
deleted theorem Finset.iInf_insert_update
deleted theorem Finset.iInf_singleton
deleted theorem Finset.iInf_union
deleted theorem Finset.iSup_biUnion
deleted theorem Finset.iSup_coe
deleted theorem Finset.iSup_finset_image
deleted theorem Finset.iSup_insert
deleted theorem Finset.iSup_insert_update
deleted theorem Finset.iSup_singleton
deleted theorem Finset.iSup_union
deleted theorem Finset.induction_on_max
deleted theorem Finset.induction_on_min
deleted theorem Finset.isGLB_iff_isLeast
deleted theorem Finset.isGLB_mem
deleted theorem Finset.isGreatest_max'
deleted theorem Finset.isLUB_mem
deleted theorem Finset.isLeast_min'
deleted theorem Finset.le_max'
deleted theorem Finset.le_max
deleted theorem Finset.le_max_of_eq
deleted theorem Finset.le_min'
deleted theorem Finset.le_min'_iff
deleted theorem Finset.lt_min'_iff
deleted theorem Finset.map_ofDual_max
deleted theorem Finset.map_ofDual_min
deleted theorem Finset.map_toDual_max
deleted theorem Finset.map_toDual_min
deleted def Finset.max'
deleted theorem Finset.max'_eq_sup'
deleted theorem Finset.max'_erase_ne_self
deleted theorem Finset.max'_image
deleted theorem Finset.max'_insert
deleted theorem Finset.max'_le
deleted theorem Finset.max'_le_iff
deleted theorem Finset.max'_lt_iff
deleted theorem Finset.max'_mem
deleted theorem Finset.max'_singleton
deleted theorem Finset.max'_subset
deleted theorem Finset.max_empty
deleted theorem Finset.max_eq_bot
deleted theorem Finset.max_eq_sup_coe
deleted theorem Finset.max_eq_sup_withBot
deleted theorem Finset.max_erase_ne_self
deleted theorem Finset.max_insert
deleted theorem Finset.max_mem_image_coe
deleted theorem Finset.max_mono
deleted theorem Finset.max_of_mem
deleted theorem Finset.max_of_nonempty
deleted theorem Finset.max_singleton
deleted theorem Finset.mem_of_max
deleted theorem Finset.mem_of_min
deleted def Finset.min'
deleted theorem Finset.min'_eq_inf'
deleted theorem Finset.min'_erase_ne_self
deleted theorem Finset.min'_image
deleted theorem Finset.min'_insert
deleted theorem Finset.min'_le
deleted theorem Finset.min'_lt_max'
deleted theorem Finset.min'_mem
deleted theorem Finset.min'_singleton
deleted theorem Finset.min'_subset
deleted theorem Finset.min_empty
deleted theorem Finset.min_eq_inf_withTop
deleted theorem Finset.min_eq_top
deleted theorem Finset.min_erase_ne_self
deleted theorem Finset.min_insert
deleted theorem Finset.min_le
deleted theorem Finset.min_le_of_eq
deleted theorem Finset.min_mem_image_coe
deleted theorem Finset.min_mono
deleted theorem Finset.min_of_mem
deleted theorem Finset.min_of_nonempty
deleted theorem Finset.min_singleton
deleted theorem Finset.not_mem_of_lt_min
deleted theorem Finset.not_mem_of_max_lt
deleted theorem Finset.ofDual_max'
deleted theorem Finset.ofDual_min'
deleted theorem Finset.set_biInter_coe
deleted theorem Finset.set_biInter_insert
deleted theorem Finset.set_biInter_inter
deleted theorem Finset.set_biUnion_coe
deleted theorem Finset.set_biUnion_insert
deleted theorem Finset.set_biUnion_union
deleted theorem Finset.toDual_max'
deleted theorem Finset.toDual_min'
deleted theorem Monotone.map_finset_max'
deleted theorem Monotone.map_finset_min'
deleted theorem iInf_eq_iInf_finset'
deleted theorem iInf_eq_iInf_finset
deleted theorem iSup_eq_iSup_finset'
deleted theorem iSup_eq_iSup_finset
added theorem Finset.coe_max'
added theorem Finset.coe_min'
added theorem Finset.isGLB_mem
added theorem Finset.isGreatest_max'
added theorem Finset.isLUB_mem
added theorem Finset.isLeast_min'
added theorem Finset.le_max'
added theorem Finset.le_max
added theorem Finset.le_max_of_eq
added theorem Finset.le_min'
added theorem Finset.le_min'_iff
added theorem Finset.lt_min'_iff
added theorem Finset.map_ofDual_max
added theorem Finset.map_ofDual_min
added theorem Finset.map_toDual_max
added theorem Finset.map_toDual_min
added def Finset.max'
added theorem Finset.max'_eq_sup'
added theorem Finset.max'_image
added theorem Finset.max'_insert
added theorem Finset.max'_le
added theorem Finset.max'_le_iff
added theorem Finset.max'_lt_iff
added theorem Finset.max'_mem
added theorem Finset.max'_singleton
added theorem Finset.max'_subset
added theorem Finset.max_empty
added theorem Finset.max_eq_bot
added theorem Finset.max_eq_sup_coe
added theorem Finset.max_insert
added theorem Finset.max_mono
added theorem Finset.max_of_mem
added theorem Finset.max_of_nonempty
added theorem Finset.max_singleton
added theorem Finset.mem_of_max
added theorem Finset.mem_of_min
added def Finset.min'
added theorem Finset.min'_eq_inf'
added theorem Finset.min'_image
added theorem Finset.min'_insert
added theorem Finset.min'_le
added theorem Finset.min'_lt_max'
added theorem Finset.min'_mem
added theorem Finset.min'_singleton
added theorem Finset.min'_subset
added theorem Finset.min_empty
added theorem Finset.min_eq_top
added theorem Finset.min_insert
added theorem Finset.min_le
added theorem Finset.min_le_of_eq
added theorem Finset.min_mono
added theorem Finset.min_of_mem
added theorem Finset.min_of_nonempty
added theorem Finset.min_singleton
added theorem Finset.ofDual_max'
added theorem Finset.ofDual_min'
added theorem Finset.toDual_max'
added theorem Finset.toDual_min'
added theorem Finset.iInf_biUnion
added theorem Finset.iInf_coe
added theorem Finset.iInf_insert
added theorem Finset.iInf_singleton
added theorem Finset.iInf_union
added theorem Finset.iSup_biUnion
added theorem Finset.iSup_coe
added theorem Finset.iSup_insert
added theorem Finset.iSup_singleton
added theorem Finset.iSup_union
added theorem Finset.set_biInter_coe
added theorem Finset.set_biUnion_coe
added theorem iInf_eq_iInf_finset'
added theorem iInf_eq_iInf_finset
added theorem iSup_eq_iSup_finset'
added theorem iSup_eq_iSup_finset