Commit 2023-01-17 10:40 94cbe78c

View on Github →

feat: port Data.Finset.Lattice (#1606)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Lattice.lean

added theorem Finset.card_le_diff_of_interleaved

added theorem Finset.card_le_of_interleaved

added theorem Finset.coe_inf'

added theorem Finset.coe_inf_of_nonempty

added theorem Finset.coe_max'

added theorem Finset.coe_min'

added theorem Finset.coe_sup'

added theorem Finset.coe_sup_of_nonempty

added theorem Finset.comp_inf'_eq_inf'_comp

added theorem Finset.comp_inf_eq_inf_comp

added theorem Finset.comp_inf_eq_inf_comp_of_is_total

added theorem Finset.comp_sup'_eq_sup'_comp

added theorem Finset.comp_sup_eq_sup_comp

added theorem Finset.comp_sup_eq_sup_comp_of_is_total

added theorem Finset.disjoint_sup_left

added theorem Finset.disjoint_sup_right

added theorem Finset.exists_max_image

added theorem Finset.exists_mem_eq_inf'

added theorem Finset.exists_mem_eq_inf

added theorem Finset.exists_mem_eq_sup'

added theorem Finset.exists_mem_eq_sup

added theorem Finset.exists_min_image

added theorem Finset.exists_nat_subset_range

added theorem Finset.exists_next_left

added theorem Finset.exists_next_right

added theorem Finset.induction_on_max

added theorem Finset.induction_on_max_value

added theorem Finset.induction_on_min

added theorem Finset.induction_on_min_value

added def Finset.inf'

added theorem Finset.inf'_bunionᵢ

added theorem Finset.inf'_congr

added theorem Finset.inf'_cons

added theorem Finset.inf'_const

added theorem Finset.inf'_eq_inf

added theorem Finset.inf'_induction

added theorem Finset.inf'_insert

added theorem Finset.inf'_le

added theorem Finset.inf'_le_iff

added theorem Finset.inf'_lt_iff

added theorem Finset.inf'_map

added theorem Finset.inf'_mem

added theorem Finset.inf'_mul_le_mul_inf'_of_nonneg

added theorem Finset.inf'_singleton

added def Finset.inf

added theorem Finset.inf_attach

added theorem Finset.inf_bunionᵢ

added theorem Finset.inf_closed_of_inf_closed

added theorem Finset.inf_coe

added theorem Finset.inf_congr

added theorem Finset.inf_cons

added theorem Finset.inf_const

added theorem Finset.inf_def

added theorem Finset.inf_empty

added theorem Finset.inf_eq_infᵢ

added theorem Finset.inf_eq_infₛ_image

added theorem Finset.inf_eq_top_iff

added theorem Finset.inf_erase_top

added theorem Finset.inf_id_eq_infₛ

added theorem Finset.inf_id_set_eq_interₛ

added theorem Finset.inf_image

added theorem Finset.inf_induction

added theorem Finset.inf_inf

added theorem Finset.inf_insert

added theorem Finset.inf_le

added theorem Finset.inf_map

added theorem Finset.inf_mem

added theorem Finset.inf_mono

added theorem Finset.inf_mono_fun

added theorem Finset.inf_of_mem

added theorem Finset.inf_product_left

added theorem Finset.inf_product_right

added theorem Finset.inf_sdiff_left

added theorem Finset.inf_sdiff_right

added theorem Finset.inf_set_eq_interᵢ

added theorem Finset.inf_singleton

added theorem Finset.inf_sup_distrib_left

added theorem Finset.inf_sup_distrib_right

added theorem Finset.inf_top

added theorem Finset.inf_union

added theorem Finset.infᵢ_bunionᵢ

added theorem Finset.infᵢ_coe

added theorem Finset.infᵢ_finset_image

added theorem Finset.infᵢ_insert

added theorem Finset.infᵢ_insert_update

added theorem Finset.infᵢ_option_toFinset

added theorem Finset.infᵢ_singleton

added theorem Finset.infᵢ_union

added theorem Finset.isGreatest_max'

added theorem Finset.isLeast_min'

added theorem Finset.is_glb_iff_is_least

added theorem Finset.is_glb_mem

added theorem Finset.is_lub_iff_is_greatest

added theorem Finset.is_lub_mem

added theorem Finset.le_inf'

added theorem Finset.le_inf'_iff

added theorem Finset.le_inf_const_le

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.le_sup'

added theorem Finset.le_sup'_iff

added theorem Finset.le_sup

added theorem Finset.lt_inf'_iff

added theorem Finset.lt_max'_of_mem_erase_max'

added theorem Finset.lt_min'_iff

added theorem Finset.lt_sup'_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'_erase_ne_self

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_eq_sup_withBot

added theorem Finset.max_erase_ne_self

added theorem Finset.max_insert

added theorem Finset.max_mem_image_coe

added theorem Finset.max_mem_insert_bot_image_coe

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 theorem Finset.mem_sup

added def Finset.min'

added theorem Finset.min'_eq_inf'

added theorem Finset.min'_erase_ne_self

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'_lt_max'_of_card

added theorem Finset.min'_lt_of_mem_erase_min'

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_inf_withTop

added theorem Finset.min_eq_top

added theorem Finset.min_erase_ne_self

added theorem Finset.min_insert

added theorem Finset.min_le

added theorem Finset.min_le_of_eq

added theorem Finset.min_mem_image_coe

added theorem Finset.min_mem_insert_top_image_coe

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.mul_inf_le_inf_mul_of_nonneg

added theorem Finset.not_mem_of_coe_lt_min

added theorem Finset.not_mem_of_lt_min

added theorem Finset.not_mem_of_max_lt

added theorem Finset.not_mem_of_max_lt_coe

added theorem Finset.ofDual_inf'

added theorem Finset.ofDual_inf

added theorem Finset.ofDual_max'

added theorem Finset.ofDual_min'

added theorem Finset.ofDual_sup'

added theorem Finset.ofDual_sup

added theorem Finset.set_binterᵢ_bunionᵢ

added theorem Finset.set_binterᵢ_coe

added theorem Finset.set_binterᵢ_finset_image

added theorem Finset.set_binterᵢ_insert

added theorem Finset.set_binterᵢ_insert_update

added theorem Finset.set_binterᵢ_inter

added theorem Finset.set_binterᵢ_option_toFinset

added theorem Finset.set_binterᵢ_singleton

added theorem Finset.set_bunionᵢ_bunionᵢ

added theorem Finset.set_bunionᵢ_coe

added theorem Finset.set_bunionᵢ_finset_image

added theorem Finset.set_bunionᵢ_insert

added theorem Finset.set_bunionᵢ_insert_update

added theorem Finset.set_bunionᵢ_option_toFinset

added theorem Finset.set_bunionᵢ_preimage_singleton

added theorem Finset.set_bunionᵢ_singleton

added theorem Finset.set_bunionᵢ_union

added theorem Finset.subset_range_sup_succ

added theorem Finset.subset_set_bunionᵢ_of_mem

added def Finset.sup'

added theorem Finset.sup'_bunionᵢ

added theorem Finset.sup'_congr

added theorem Finset.sup'_cons

added theorem Finset.sup'_const

added theorem Finset.sup'_eq_sup

added theorem Finset.sup'_induction

added theorem Finset.sup'_insert

added theorem Finset.sup'_le

added theorem Finset.sup'_le_iff

added theorem Finset.sup'_lt_iff

added theorem Finset.sup'_map

added theorem Finset.sup'_mem

added theorem Finset.sup'_mul_le_mul_sup'_of_nonneg

added theorem Finset.sup'_singleton

added def Finset.sup

added theorem Finset.sup_attach

added theorem Finset.sup_bot

added theorem Finset.sup_bunionᵢ

added theorem Finset.sup_closed_of_sup_closed

added theorem Finset.sup_coe

added theorem Finset.sup_congr

added theorem Finset.sup_cons

added theorem Finset.sup_const

added theorem Finset.sup_const_le

added theorem Finset.sup_def

added theorem Finset.sup_empty

added theorem Finset.sup_eq_bot_iff

added theorem Finset.sup_eq_bunionᵢ

added theorem Finset.sup_eq_supᵢ

added theorem Finset.sup_eq_supₛ_image

added theorem Finset.sup_erase_bot

added theorem Finset.sup_finset_image

added theorem Finset.sup_id_eq_supₛ

added theorem Finset.sup_id_set_eq_unionₛ

added theorem Finset.sup_image

added theorem Finset.sup_induction

added theorem Finset.sup_inf_distrib_left

added theorem Finset.sup_inf_distrib_right

added theorem Finset.sup_insert

added theorem Finset.sup_ite

added theorem Finset.sup_le_of_le_directed

added theorem Finset.sup_map

added theorem Finset.sup_mem

added theorem Finset.sup_mono

added theorem Finset.sup_mono_fun

added theorem Finset.sup_mul_le_mul_sup_of_nonneg

added theorem Finset.sup_of_mem

added theorem Finset.sup_product_left

added theorem Finset.sup_product_right

added theorem Finset.sup_sdiff_left

added theorem Finset.sup_sdiff_right

added theorem Finset.sup_set_eq_bunionᵢ

added theorem Finset.sup_singleton''

added theorem Finset.sup_singleton'

added theorem Finset.sup_singleton

added theorem Finset.sup_sup

added theorem Finset.sup_toFinset

added theorem Finset.sup_union

added theorem Finset.supᵢ_bunionᵢ

added theorem Finset.supᵢ_coe

added theorem Finset.supᵢ_finset_image

added theorem Finset.supᵢ_insert

added theorem Finset.supᵢ_insert_update

added theorem Finset.supᵢ_option_toFinset

added theorem Finset.supᵢ_singleton

added theorem Finset.supᵢ_union

added theorem Finset.toDual_inf'

added theorem Finset.toDual_inf

added theorem Finset.toDual_max'

added theorem Finset.toDual_min'

added theorem Finset.toDual_sup'

added theorem Finset.toDual_sup

added theorem List.foldr_inf_eq_inf_toFinset

added theorem List.foldr_sup_eq_sup_toFinset

added theorem Multiset.count_finset_sup

added theorem Multiset.map_finset_sup

added theorem Multiset.mem_sup

added theorem Set.interᵢ_eq_interᵢ_finset'

added theorem Set.interᵢ_eq_interᵢ_finset

added theorem Set.unionᵢ_eq_unionᵢ_finset'

added theorem Set.unionᵢ_eq_unionᵢ_finset

added theorem infᵢ_eq_infᵢ_finset'

added theorem infᵢ_eq_infᵢ_finset

added theorem supᵢ_eq_supᵢ_finset'

added theorem supᵢ_eq_supᵢ_finset