Commit 2023-01-21 14:50 5841a8d1

View on Github →

feat: port Data.Set.Finite (#1734)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Finite.lean

added theorem Finite.Set.finite_bunionᵢ

added theorem Finset.finite_to_set

added theorem Finset.finite_to_set_toFinset

added theorem List.finite_to_set

added theorem Multiset.finite_to_set

added theorem Multiset.finite_to_set_toFinset

added theorem Set.Finite.bddAbove_bunionᵢ

added theorem Set.Finite.bddBelow_bunionᵢ

added theorem Set.Finite.bind

added theorem Set.Finite.bunionᵢ'

added theorem Set.Finite.bunionᵢ

added theorem Set.Finite.card_toFinset

added theorem Set.Finite.coeSort_toFinset

added theorem Set.Finite.dependent_image

added theorem Set.Finite.diff

added theorem Set.Finite.dinduction_on

added theorem Set.Finite.exists_finset

added theorem Set.Finite.exists_finset_coe

added theorem Set.Finite.exists_lt_map_eq_of_forall_mem

added theorem Set.Finite.exists_maximal_wrt

added theorem Set.Finite.fin_embedding

added theorem Set.Finite.fin_param

added theorem Set.Finite.finite_of_compl

added theorem Set.Finite.finite_subsets

added theorem Set.Finite.image2

added theorem Set.Finite.image

added theorem Set.Finite.induction_on'

added theorem Set.Finite.induction_on

added theorem Set.Finite.inf_of_left

added theorem Set.Finite.inf_of_right

added theorem Set.Finite.infinite_compl

added theorem Set.Finite.infᵢ_bsupr_of_antitone

added theorem Set.Finite.infᵢ_bsupr_of_monotone

added theorem Set.Finite.insert

added theorem Set.Finite.inter_of_left

added theorem Set.Finite.inter_of_right

added theorem Set.Finite.interₛ

added theorem Set.Finite.map

added theorem Set.Finite.of_diff

added theorem Set.Finite.of_finite_image

added theorem Set.Finite.of_preimage

added theorem Set.Finite.of_subsingleton

added theorem Set.Finite.offDiag

added theorem Set.Finite.pi

added theorem Set.Finite.preimage

added theorem Set.Finite.preimage_embedding

added theorem Set.Finite.prod

added theorem Set.Finite.sSubset_toFinset

added theorem Set.Finite.sep

added theorem Set.Finite.seq'

added theorem Set.Finite.seq

added theorem Set.Finite.subset

added theorem Set.Finite.subset_toFinset

added theorem Set.Finite.sup

added theorem Set.Finite.supᵢ_binfi_of_antitone

added theorem Set.Finite.supᵢ_binfi_of_monotone

added theorem Set.Finite.toFinset_insert'

added theorem Set.Finite.toFinset_insert

added theorem Set.Finite.toFinset_offDiag

added theorem Set.Finite.toFinset_prod

added theorem Set.Finite.toFinset_sSubset

added theorem Set.Finite.toFinset_singleton

added theorem Set.Finite.toFinset_subset

added theorem Set.Finite.union

added theorem Set.Finite.unionₛ

added inductive Set.Finite

added theorem Set.Infinite.diff

added theorem Set.Infinite.exists_lt_map_eq_of_mapsTo

added theorem Set.Infinite.exists_nat_lt

added theorem Set.Infinite.exists_ne_map_eq_of_mapsTo

added theorem Set.Infinite.exists_not_mem_finset

added theorem Set.Infinite.exists_subset_card_eq

added theorem Set.Infinite.nonempty

added def Set.Nat.fintypeIio

added theorem Set.Subsingleton.finite

added theorem Set.card_fintypeInsertOfNotMem

added theorem Set.card_image_of_inj_on

added theorem Set.card_image_of_injective

added theorem Set.card_insert

added theorem Set.card_le_of_subset

added theorem Set.card_lt_card

added theorem Set.card_ne_eq

added theorem Set.card_range_of_injective

added theorem Set.card_singleton

added theorem Set.empty_card'

added theorem Set.empty_card

added theorem Set.eq_finite_unionᵢ_of_finite_subset_unionᵢ

added theorem Set.eq_of_subset_of_card_le

added theorem Set.exists_finite_iff_finset

added theorem Set.exists_lower_bound_image

added theorem Set.exists_max_image

added theorem Set.exists_min_image

added theorem Set.exists_upper_bound_image

added theorem Set.finite_coe_iff

added theorem Set.finite_def

added theorem Set.finite_empty

added theorem Set.finite_image_fst_and_snd_iff

added theorem Set.finite_image_iff

added theorem Set.finite_isBot

added theorem Set.finite_isTop

added theorem Set.finite_le_nat

added theorem Set.finite_lt_nat

added theorem Set.finite_mem_finset

added theorem Set.finite_of_finite_preimage

added theorem Set.finite_of_forall_between_eq_endpoints

added theorem Set.finite_option

added theorem Set.finite_preimage_inl_and_inr

added theorem Set.finite_pure

added theorem Set.finite_range

added theorem Set.finite_range_const

added theorem Set.finite_range_findGreatest

added theorem Set.finite_range_ite

added theorem Set.finite_singleton

added theorem Set.finite_subset_unionᵢ

added theorem Set.finite_union

added theorem Set.finite_unionᵢ

added theorem Set.finite_univ

added theorem Set.finite_univ_iff

added def Set.fintypeBUnionᵢ

added def Set.fintypeBind

added def Set.fintypeInsertOfMem

added def Set.fintypeInsertOfNotMem

added def Set.fintypeOfFintypeImage

added def Set.fintypeSubset

added theorem Set.forall_finite_image_eval_iff

added theorem Set.infinite_coe_iff

added theorem Set.infinite_image_iff

added theorem Set.infinite_of_finite_compl

added theorem Set.infinite_of_infinite_image

added theorem Set.infinite_of_injOn_mapsTo

added theorem Set.infinite_of_injective_forall_mem

added theorem Set.infinite_of_not_bddAbove

added theorem Set.infinite_of_not_bddBelow

added theorem Set.infinite_range_of_injective

added theorem Set.infinite_union

added theorem Set.infinite_univ

added theorem Set.infinite_univ_iff

added theorem Set.infᵢ_supᵢ_of_antitone

added theorem Set.infᵢ_supᵢ_of_monotone

added theorem Set.interᵢ_unionᵢ_of_antitone

added theorem Set.interᵢ_unionᵢ_of_monotone

added theorem Set.not_infinite

added theorem Set.not_injOn_infinite_finite_image

added theorem Set.seq_of_forall_finite_exists

added theorem Set.supᵢ_infᵢ_of_antitone

added theorem Set.supᵢ_infᵢ_of_monotone

added theorem Set.toFinite

added theorem Set.union_finset_finite_of_range_finite

added theorem Set.unionᵢ_interᵢ_of_antitone

added theorem Set.unionᵢ_interᵢ_of_monotone

added theorem Set.unionᵢ_pi_of_monotone

added theorem Set.unionᵢ_univ_pi_of_monotone

added theorem Set.univ_finite_iff_nonempty_fintype