Theoremsfinite_diff, finite_image, finite_insert, finite_inter_of_left, finite_inter_of_right, finite_sep, finite_union, subset, of_finite_univ, of_forall_not_lt_lt, exists, exists_card_eq, exists_notMem, exists_subset_injOn_image_eq_of_surjOn, finite_toSet, finite_toSet_toFinset, forall, finite_toSet, finite_toSet, finite_toSet_toFinset, finsetSetFinite_apply_coe, finsetSetFinite_symm_apply, finite_iff_finite, card_toFinset, coeSort_toFinset, coe_toFinset, diff, disjoint_toFinset, exists_finset, exists_finset_coe, exists_notMem, finite_of_compl, image, induction_on, induction_on_subset, inf_of_left, inf_of_right, infinite_compl, injOn_iff_bijOn_of_mapsTo, insert, inter_of_left, inter_of_right, map, mem_toFinset, nonempty_fintype, ofFinset, of_diff, of_finite_image, of_injOn, of_preimage, of_subsingleton, of_surjOn, preimage, preimage_embedding, sep, ssubset_toFinset, subset, subset_toFinset, subtypeEquivToFinset_apply_coe, subtypeEquivToFinset_symm_apply_coe, sup, surjOn_iff_bijOn_of_mapsTo, symmDiff, symmDiff_congr, toFinset_compl, toFinset_diff, toFinset_empty, toFinset_eq_empty, toFinset_eq_toFinset, toFinset_eq_univ, toFinset_image, toFinset_inj, toFinset_insert, toFinset_insert', toFinset_inter, toFinset_mono, toFinset_nonempty, toFinset_nontrivial, toFinset_range, toFinset_setOf, toFinset_singleton, toFinset_ssubset, toFinset_ssubset_toFinset, toFinset_strictMono, toFinset_subset, toFinset_subset_toFinset, toFinset_symmDiff, toFinset_union, toFinset_univ, union, diff, exists_ne_map_eq_of_mapsTo, exists_notMem_finite, exists_notMem_finset, exists_subset_card_eq, image, mono, nonempty, nontrivial, of_image, preimage, preimage', finite, card_empty, card_fintypeInsertOfNotMem, card_image_of_inj_on, card_image_of_injective, card_insert, card_le_card, card_lt_card, card_ne_eq, card_range_of_injective, card_singleton, eq_of_subset_of_card_le, exists_finite_iff_finset, exists_subset_image_finite_and, finite_def, finite_empty, finite_image_iff, finite_insert, finite_le_nat, finite_lt_nat, finite_mem_finset, finite_of_finite_preimage, finite_of_forall_not_lt_lt, finite_option, finite_preimage_inl_and_inr, finite_range_const, finite_range_findGreatest, finite_range_iff, finite_range_ite, finite_singleton, finite_union, finite_univ, finite_univ_iff, infinite_image_iff, infinite_of_finite_compl, infinite_of_injOn_mapsTo, infinite_of_injective_forall_mem, infinite_range_iff, infinite_range_of_injective, infinite_union, infinite_univ, infinite_univ_iff, instCanLiftFinsetCoeFinite, not_injOn_infinite_finite_image, seq_of_forall_finite_exists, toFinite_toFinset, univ_finite_iff_nonempty_fintype, instWellFoundedLTSubtypeSetFinite | 150 |