Sets

📁 Source: Mathlib/Data/Fintype/Sets.lean

Statistics

Metric	Count
Definitions fintype, fintypeCoeSort, fintype, finsetEquivSet, finsetOrderIsoSet, fintype, fintype, fintype, decidableMemOfFintype, toFinset, fintype, finsetStx, precheckFinsetStx, setFintype	14
Theorems attach_eq_univ, toFinset_coe, univ_eq_attach, coe_finsetEquivSet, coe_finsetOrderIsoSet, coe_finsetOrderIsoSet_symm, coe_image_univ, finsetEquivSet_apply, finsetEquivSet_symm_apply, finsetOrderIsoSet_toEquiv, univ_Prop, toFinset_nonempty_of_nonempty, coe_toFinset, disjoint_toFinset, filter_mem_univ_eq_toFinset, mem_toFinset, ssubset_toFinset, subset_toFinset, subsingleton_toFinset_iff, toFinset_compl, toFinset_congr, toFinset_diff, toFinset_empty, toFinset_eq_empty, toFinset_eq_univ, toFinset_image, toFinset_inj, toFinset_insert, toFinset_inter, toFinset_mono, toFinset_nonempty, toFinset_nontrivial, toFinset_ofFinset, toFinset_range, toFinset_setOf, toFinset_singleton, toFinset_ssubset, toFinset_ssubset_toFinset, toFinset_ssubset_univ, toFinset_strict_mono, toFinset_subset, toFinset_subset_toFinset, toFinset_subset_toFinset_of_subset, toFinset_symmDiff, toFinset_union, toFinset_univ, mem_image_univ_iff_mem_range	47
Total	61

Finset

Definitions

Name	Category	Theorems
fintypeCoeSort 📖	CompOp	1 math math: univ_eq_attach

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
attach_eq_univ 📖	mathematical	—	attach univ Finset instMembership Subtype.fintype	—	—
toFinset_coe 📖	mathematical	—	Set.toFinset SetLike.coe Finset instSetLike	—	ext Set.mem_toFinset
univ_eq_attach 📖	mathematical	—	univ Finset SetLike.instMembership instSetLike fintypeCoeSort attach	—	—

Finset.Subtype

Definitions

Name	Category	Theorems
fintype 📖	CompOp	102 math math: RootPairing.GeckConstruction.isSl2Triple, RootPairing.GeckConstruction.instHasTrivialRadical, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, Finset.attach_eq_univ, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, Finset.prod_eq_prod_extend, RootPairing.GeckConstruction.trace_h_eq_zero, Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod, Submodule.mem_span_image_iff_exists_fun, MeasureTheory.integral_infinitePi_of_piFinset, Equiv.Perm.OnCycleFactors.kerParam_range_card, MeasureTheory.lintegral_restrict_infinitePi, MeasureTheory.volume_preserving_piFinsetUnion, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LinearMap.trace_eq_matrix_trace_of_finset, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux_assoc, MeasureTheory.Measure.isProjectiveLimit_infinitePi, MeasureTheory.piContent_cylinder, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, LinearMap.det_def, MeasureTheory.Measure.map_piSingleton, RootPairing.GeckConstruction.lie_h_e, MeasureTheory.Measure.pi_prod_map_IocProdIoc, Equiv.Perm.Basis.card_ofPermHom_support, MeasureTheory.isProjectiveMeasureFamily_pi, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_π_app_eq_sum, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LinearMap.det_eq_det_toMatrix_of_finset, Finset.prod_coe_sort, Finset.prod_apply_dite, RootPairing.GeckConstruction.span_range_h'_eq_top, MeasureTheory.Measure.pi_prod_map_IicProdIoc, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, Submodule.mem_span_finset', RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', MeasureTheory.partialTraj_const, Finset.sum_pow_of_commute, Finset.centroid_univ, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, RootPairing.GeckConstruction.ω_mul_h, exists_orthonormalBasis, RootPairing.GeckConstruction.instIsIrreducible, Finset.inclusion_exclusion_card_biUnion, Equiv.Perm.Basis.ofPermHom_support, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, Finset.prod_dite_of_false, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, RootPairing.GeckConstruction.ωConj_invFun, Finset.prod_coe_sort_eq_attach, Nat.prod_pow_primeFactors_factorization, RootPairing.GeckConstruction.isNilpotent_f, Finset.sum_dite_of_false, RootPairing.GeckConstruction.lie_e_f_same, MeasureTheory.Measure.isProjectiveLimit_infinitePiNat, RootPairing.GeckConstruction.ω_mul_ω, RootPairing.GeckConstruction.f_lie_v_ne, RootPairing.GeckConstruction.ωConj_toFun, RootPairing.GeckConstruction.e_lie_v_ne, RootPairing.GeckConstruction.ω_mul_e, RootPairing.GeckConstruction.isNilpotent_e, RootPairing.GeckConstruction.h_mem_lieAlgebra, Finset.inclusion_exclusion_sum_biUnion, OrthonormalBasis.span_apply, MeasureTheory.measurePreserving_piFinsetUnion, Finset.prod_dite, RootPairing.GeckConstruction.lie_h_f, RootPairing.GeckConstruction.ω_mul_f, MeasureTheory.Measure.infinitePiNat_map_restrict, MeasureTheory.Measure.infinitePi_cylinder, Finset.attach_affineCombination_of_injective, MeasureTheory.partialTraj_const_restrict₂, RootPairing.GeckConstruction.lie_e_lie_f_apply, RootPairing.GeckConstruction.f_lie_v_same, Finset.sum_apply_dite, LinearMap.coe_det, Submonoid.mem_closure_finset', MeasureTheory.Measure.infinitePi_map_restrict, Finset.sum_dite_of_true, Equiv.Perm.CycleType.count_def, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, RootPairing.GeckConstruction.f_mem_lieAlgebra, RootPairing.GeckConstruction.e_mem_lieAlgebra, RootPairing.GeckConstruction.lie_h_h, Finset.sum_coe_sort_eq_attach, AddSubmonoid.mem_closure_finset', LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, Orthonormal.exists_orthonormalBasis_extension, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, Equiv.Perm.support_subtypePerm, finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply, Finset.sum_coe_sort, RootPairing.GeckConstruction.lie_e_f_mul_ω, Finset.sum_eq_sum_extend, RootPairing.GeckConstruction.e_lie_u, RootPairing.GeckConstruction.lie_e_f_ne, Finset.sum_dite, Equiv.Perm.commute_ofSubtype_noncommPiCoprod, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply, Finset.prod_dite_of_true

FinsetCoe

Definitions

Name	Category	Theorems
fintype 📖	CompOp	6 math math: hasSum_sum_support_of_ne_finset_zero, hasProd_prod_support_of_ne_finset_one, Finset.hasSum_support, Finset.hasProd_support, Finset.prod_finset_coe, Finset.sum_finset_coe

Fintype

Definitions

Name	Category	Theorems
finsetEquivSet 📖	CompOp	5 math math: coe_finsetEquivSet, finsetEquivSet_apply, coe_finsetOrderIsoSet_symm, finsetOrderIsoSet_toEquiv, finsetEquivSet_symm_apply
finsetOrderIsoSet 📖	CompOp	3 math math: coe_finsetOrderIsoSet_symm, coe_finsetOrderIsoSet, finsetOrderIsoSet_toEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_finsetEquivSet 📖	mathematical	—	DFunLike.coe Equiv Finset Set EquivLike.toFunLike Equiv.instEquivLike finsetEquivSet SetLike.coe Finset.instSetLike	—	—
coe_finsetOrderIsoSet 📖	mathematical	—	DFunLike.coe OrderIso Finset Set Preorder.toLE PartialOrder.toPreorder Finset.partialOrder Set.instLE instFunLikeOrderIso finsetOrderIsoSet SetLike.coe Finset.instSetLike	—	—
coe_finsetOrderIsoSet_symm 📖	mathematical	—	DFunLike.coe OrderIso Set Finset Set.instLE Preorder.toLE PartialOrder.toPreorder Finset.partialOrder instFunLikeOrderIso OrderIso.symm finsetOrderIsoSet Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm finsetEquivSet	—	—
coe_image_univ 📖	mathematical	—	SetLike.coe Finset Finset.instSetLike Finset.image Finset.univ Set.range	—	Finset.coe_image Finset.coe_univ Set.image_univ
finsetEquivSet_apply 📖	mathematical	—	DFunLike.coe Equiv Finset Set EquivLike.toFunLike Equiv.instEquivLike finsetEquivSet SetLike.coe Finset.instSetLike	—	—
finsetEquivSet_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Set Finset EquivLike.toFunLike Equiv.instEquivLike Equiv.symm finsetEquivSet Set.toFinset	—	—
finsetOrderIsoSet_toEquiv 📖	mathematical	—	RelIso.toEquiv Finset Set Preorder.toLE PartialOrder.toPreorder Finset.partialOrder Set.instLE finsetOrderIsoSet finsetEquivSet	—	—
univ_Prop 📖	mathematical	—	Finset.univ Prop.fintype Finset Finset.instInsert LinearOrder.toDecidableEq Prop.linearOrder Finset.instSingleton	—	Finset.eq_of_veq Multiset.ndinsert_of_notMem

List.Subtype

Definitions

Name	Category	Theorems
fintype 📖	CompOp	2 math math: List.cycleType_formPerm, List.cycleOf_formPerm

Multiset.Subtype

Definitions

Name	Category	Theorems
fintype 📖	CompOp	2 math math: Finset.sum_mem_multiset, Finset.prod_mem_multiset

Prop

Definitions

Name	Category	Theorems
fintype 📖	CompOp	4 math math: Fintype.univ_Prop, Fintype.prod_Prop, Fintype.card_prop, Fintype.sum_Prop

Set

Definitions

Name	Category	Theorems
decidableMemOfFintype 📖	CompOp	—
toFinset 📖	CompOp	112 math math: toFinset_Icc, FormalMultilinearSeries.comp_rightInv_aux1, finrank_span_set_eq_card, quadraticChar_card_sqrts, toFinset_union, einfsep_of_fintype, SimpleGraph.edgeFinset_subset_sym2_of_support_subset, subsingleton_toFinset_iff, subset_toFinset, toFinset_compl, SimpleGraph.edgeFinset_top, toFinset_Ioi, toFinset_range, toFinset_ssubset_toFinset, toFinset_symmDiff, hasSum_sum_support_of_ne_finset_zero, ConjRootClass.minpoly.map_eq_prod, hasProd_prod_support_of_ne_finset_one, SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset, filter_mem_univ_eq_toFinset, image_range_addOrderOf, toFinset_eq_empty, OrderIso.infIrredUpperSet_symm_apply, toFinset_Ioo, toFinset_diff, toFinset_Iic, toFinset_inj, Finset.hasSum_support, hasProd_fintype_support, Finset.toFinset_coe, Nontrivial.infsep_of_fintype, OrderIso.supIrredLowerSet_symm_apply, toFinset_congr, toFinset_zero, finrank_span_le_card, disjoint_toFinset, toFinset_Ici, toFinset_Ico, toFinset_vadd_set, toFinset_image2, sum_conjClasses_card_eq_card, toFinset_vsub, toFinite_toFinset, toFinset_smul, hasSum_fintype_support, toFinset_Ioc, infsep_of_fintype, toFinset_eq_univ, toFinset_offDiag, toFinset_nonempty, toFinset_card, toFinset_image, toFinset_insert, toFinset_singleton, toFinset_empty, Finite.toFinset_eq_toFinset, ncard_eq_toFinset_card', SimpleGraph.set_walk_length_toFinset_eq, toFinset_subset, toFinset_ofFinset, toFinset_add, toFinset_strict_mono, encard_eq_coe_toFinset_card, SimpleGraph.Subgraph.IsSpanning.card_verts, Finset.hasProd_support, toFinset_inter, toFinset_off_diag, toFinset_ssubset, SimpleGraph.map_neighborFinset_induce, ssubset_toFinset, SimpleGraph.sum_degrees_support_eq_twice_card_edges, Finset.prod_set_coe, Finset.sum_toFinset_eq_subtype, ConjRootClass.aroots_minpoly_eq_carrier_val, Ideal.map_algebraMap_eq_finset_prod_pow, ConjRootClass.carrier_eq_mk_aroots_minpoly, FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1, toFinset_iUnion, legendreSym.card_sqrts, image_range_orderOf, Nat.card_eq_card_toFinset, toFinset_subset_toFinset, toFinset_univ, toFinset_nontrivial, toFinset_mul, toFinset_one, SimpleGraph.Subgraph.finset_card_neighborSet_eq_degree, toFinset_ssubset_univ, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, toFinset_vadd, mem_toFinset, toFinset_subset_toFinset_of_subset, Lagrange.nodal_subgroup_eq_X_pow_card_sub_one, Finset.sum_set_coe, SimpleGraph.card_neighborSet_union_compl_neighborSet, toFinset_smul_set, toFinset_mono, Aesop.toFinset_nonempty_of_nonempty, FormalMultilinearSeries.rightInv_coeff, Finset.prod_toFinset_eq_subtype, FormalMultilinearSeries.comp_rightInv_aux2, Group.card_center_add_sum_card_noncenter_eq_card, SimpleGraph.Subgraph.IsMatching.even_card, toFinset_Iio, toFinset_setOf, finsum_mem_eq_toFinset_sum, SimpleGraph.neighborFinset_def, SimpleGraph.map_edgeFinset_induce, toFinset_prod, Fintype.finsetEquivSet_symm_apply, finprod_mem_eq_toFinset_prod, coe_toFinset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toFinset 📖	mathematical	—	SetLike.coe Finset Finset.instSetLike toFinset	—	ext mem_toFinset
disjoint_toFinset 📖	mathematical	—	Disjoint Finset Finset.partialOrder Finset.instOrderBot toFinset Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra	—	coe_toFinset
filter_mem_univ_eq_toFinset 📖	mathematical	—	Finset.filter Set instMembership Finset.univ toFinset	—	Finset.ext Finset.mem_filter_univ mem_toFinset
mem_toFinset 📖	mathematical	—	Finset Finset.instMembership toFinset Set instMembership	—	—
ssubset_toFinset 📖	mathematical	—	Finset Finset.instHasSSubset toFinset Set instHasSSubset SetLike.coe Finset.instSetLike	—	Finset.coe_ssubset coe_toFinset
subset_toFinset 📖	mathematical	—	Finset Finset.instHasSubset toFinset Set instHasSubset SetLike.coe Finset.instSetLike	—	Finset.coe_subset coe_toFinset
subsingleton_toFinset_iff 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike toFinset Subsingleton	—	—
toFinset_compl 📖	mathematical	—	toFinset Compl.compl Set instCompl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra	—	Finset.ext
toFinset_congr 📖	mathematical	—	toFinset	—	Lean.Meta.FastSubsingleton.elim Fintype.instFastSubsingleton
toFinset_diff 📖	mathematical	—	toFinset Set instSDiff Finset Finset.instSDiff	—	Finset.ext
toFinset_empty 📖	mathematical	—	toFinset Set instEmptyCollection Finset Finset.instEmptyCollection	—	Finset.ext
toFinset_eq_empty 📖	mathematical	—	toFinset Finset Finset.instEmptyCollection Set instEmptyCollection	—	instIsEmptyElemEmptyCollection toFinset_empty
toFinset_eq_univ 📖	mathematical	—	toFinset Finset.univ univ	—	coe_toFinset Finset.coe_univ
toFinset_image 📖	mathematical	—	toFinset image Finset.image	—	Finset.coe_injective coe_toFinset Finset.coe_image
toFinset_inj 📖	mathematical	—	toFinset	—	coe_toFinset toFinset_congr
toFinset_insert 📖	mathematical	—	toFinset Set instInsert Finset Finset.instInsert	—	Finset.ext
toFinset_inter 📖	mathematical	—	toFinset Set instInter Finset Finset.instInter	—	Finset.ext
toFinset_mono 📖	mathematical	Set instHasSubset	Finset Finset.instHasSubset toFinset	—	toFinset_subset_toFinset
toFinset_nonempty 📖	mathematical	—	Finset.Nonempty toFinset Nonempty	—	Finset.coe_nonempty coe_toFinset
toFinset_nontrivial 📖	mathematical	—	Finset.Nontrivial toFinset Nontrivial	—	Finset.Nontrivial.eq_1 coe_toFinset
toFinset_ofFinset 📖	mathematical	Finset Finset.instMembership Set instMembership	toFinset Fintype.ofFinset	—	Finset.ext mem_toFinset
toFinset_range 📖	mathematical	—	toFinset range Finset.image Finset.univ	—	Finset.ext
toFinset_setOf 📖	mathematical	—	toFinset setOf Finset.filter Finset.univ	—	Finset.ext
toFinset_singleton 📖	mathematical	—	toFinset Set instSingletonSet Finset Finset.instSingleton	—	Finset.ext
toFinset_ssubset 📖	mathematical	—	Finset Finset.instHasSSubset toFinset Set instHasSSubset SetLike.coe Finset.instSetLike	—	Finset.coe_ssubset coe_toFinset
toFinset_ssubset_toFinset 📖	mathematical	—	Finset Finset.instHasSSubset toFinset Set instHasSSubset	—	—
toFinset_ssubset_univ 📖	mathematical	—	Finset Finset.instHasSSubset toFinset Finset.univ Set instHasSSubset univ	—	Finset.coe_univ
toFinset_strict_mono 📖	mathematical	Set instHasSSubset	Finset Finset.instHasSSubset toFinset	—	toFinset_ssubset_toFinset
toFinset_subset 📖	mathematical	—	Finset Finset.instHasSubset toFinset Set instHasSubset SetLike.coe Finset.instSetLike	—	Finset.coe_subset coe_toFinset
toFinset_subset_toFinset 📖	mathematical	—	Finset Finset.instHasSubset toFinset Set instHasSubset	—	—
toFinset_subset_toFinset_of_subset 📖	mathematical	Set instHasSubset	Finset Finset.instHasSubset toFinset	—	toFinset_mono
toFinset_symmDiff 📖	mathematical	—	toFinset symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra instSDiff Finset Finset.instLattice Finset.instSDiff	—	Finset.ext
toFinset_union 📖	mathematical	—	toFinset Set instUnion Finset Finset.instUnion	—	Finset.ext
toFinset_univ 📖	mathematical	—	toFinset univ Finset.univ	—	Finset.ext

Set.Aesop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFinset_nonempty_of_nonempty 📖	mathematical	Set.Nonempty	Finset.Nonempty Set.toFinset	—	Set.toFinset_nonempty

Subtype

Definitions

Name	Category	Theorems
fintype 📖	CompOp	170 math math: NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', NumberField.mixedEmbedding.fundamentalDomain_integerLattice, FormalMultilinearSeries.comp_rightInv_aux1, Fintype.prod_fiberwise', quadraticChar_card_sqrts, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, Fintype.prod_dite, NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace, SimpleGraph.edgeFinset_subset_sym2_of_support_subset, Sym2.card_subtype_not_diag, NumberField.mixedEmbedding.norm_le_convexBodySumFun, NumberField.Units.regOfFamily_eq_det, SimpleGraph.edgeFinset_top, SimpleGraph.map_edgeFinset_induce_of_support_subset, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, Equiv.Perm.sign_subtypePerm, Matrix.toBlock_mul_eq_add, Equiv.Perm.OnCycleFactors.kerParam_range_card, char_dvd_card_solutions_of_add_lt, Matrix.charmatrix_toSquareBlock, NumberField.mixedEmbedding.instNoAtomsMixedSpaceVolume, SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset, NumberField.mixedEmbedding.convexBodyLT_volume, LinearMap.rank_diagonal, NumberField.mixedEmbedding.convexBodySumFun_apply', SimpleGraph.card_commonNeighbors_le_degree_left, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, Algebra.Norm.Transitivity.comp_det_mul_pow, SimpleGraph.IsSRGWith.card_neighborFinset_union_eq, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, Equiv.Perm.sign_of_cycleType_eq_replicate, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, Finset.hasSum_support, hasProd_fintype_support, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, SimpleGraph.ConnectedComponent.even_card_of_isPerfectMatching, SimpleGraph.Adj.card_commonNeighbors_lt_degree, Fintype.sum_eq_add_sum_subtype_ne, NumberField.Units.instZLattice_unitLattice, Equiv.Perm.cycleType_ofSubtype, NumberField.Units.regulator_eq_det, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm, Equiv.Perm.card_fixedPoints_modEq, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, Matrix.toBlock_mul_eq_mul, Fintype.card_fin_lt_of_le, hasSum_fintype_support, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.mixedEmbedding.volume_preserving_negAt, AddGroup.card_nsmul_eq_card_nsmul_card_univ, SimpleGraph.card_commonNeighbors_le_degree_right, NumberField.Units.regOfFamily_of_isMaxRank, SimpleGraph.map_neighborFinset_induce_of_neighborSet_subset, Equiv.Perm.support_ofSubtype, SimpleGraph.degree_induce_support, Equiv.Perm.sign_of_pow_two_eq_one, Matrix.twoBlockTriangular_det, Matrix.twoBlockTriangular_det', NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, CategoryTheory.HomOrthogonal.matrixDecomposition_comp, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_one, Equiv.Perm.card_fixedPoints, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, Matrix.det_toBlock, NumberField.mixedEmbedding.det_matrixToStdBasis, Sym2.card_diagSet_compl, NumberField.mixedEmbedding.covolume_integerLattice, Finset.hasProd_support, DomMulAct.stabilizer_card', NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply, SimpleGraph.card_commonNeighbors_lt_card_verts, SimpleGraph.map_neighborFinset_induce, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, Fintype.prod_subtype_mul_prod_subtype, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, SimpleGraph.card_support_deleteIncidenceSet, char_dvd_card_solutions, NumberField.Units.abs_det_eq_abs_det, char_dvd_card_solutions_of_sum_lt, NumberField.mixedEmbedding.volume_negAt_plusPart, NumberField.mixedEmbedding.convexBodyLT'_volume, NumberField.InfinitePlace.sum_eq_sum_add_sum, NumberField.InfinitePlace.card_real_embeddings, Matrix.BlockTriangular.det, SimpleGraph.IsSRGWith.of_adj, Matrix.rank_diagonal, SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_adj_compl, SimpleGraph.sum_degrees_support_eq_twice_card_edges, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, SimpleGraph.degree_induce_of_neighborSet_subset, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, NumberField.mixedEmbedding.volume_eq_zero, Finset.sum_toFinset_eq_subtype, Fintype.card_subtype_eq_or_eq_of_ne, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1, NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm, Fin.card_range_le, legendreSym.card_sqrts, Group.card_pow_eq_card_pow_card_univ, Fintype.sum_fiberwise, Matrix.equiv_block_det, NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, SimpleGraph.card_commonNeighbors_top, Matrix.BlockTriangular.inv_toBlock, Finset.prod_congr_set, image_subtype_univ_ssubset_image_univ, NumberField.InfinitePlace.prod_eq_prod_mul_prod, Matrix.det_toSquareBlock_id, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, Sym2.card_subtype_diag, SimpleGraph.card_edgeFinset_induce_support, Fintype.card_finset_len, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume, SimpleGraph.degree_induce_of_support_subset, Equiv.Perm.CycleType.count_def, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, Finset.sum_congr_set, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, Matrix.IsHermitian.rank_eq_card_non_zero_eigs, MeasureTheory.measurePreserving_piEquivPiSubtypeProd, MvPolynomial.esymm_eq_sum_subtype, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, image_subtype_ne_univ_eq_image_erase, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, NumberField.mixedEmbedding.convexBodySum_volume, Fintype.sum_fiberwise', NumberField.Units.regulator_eq_det', Equiv.Perm.sign_subtypeCongr, FormalMultilinearSeries.rightInv_coeff, Fintype.sum_subtype_add_sum_subtype, Matrix.BlockTriangular.det_fintype, Finset.prod_toFinset_eq_subtype, FormalMultilinearSeries.comp_rightInv_aux2, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_not_adj_compl, SimpleGraph.card_edgeFinset_induce_of_support_subset, NumberField.InfinitePlace.card_complex_embeddings, DomMulAct.stabilizer_card, MeasureTheory.volume_preserving_piEquivPiSubtypeProd, NumberField.Units.basisOfIsMaxRank_fundSystem, NumberField.Units.regOfFamily_eq_det', SimpleGraph.Walk.IsEulerian.card_odd_degree, NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm, SimpleGraph.map_edgeFinset_induce, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, Matrix.BlockTriangular.charpoly, Equiv.Perm.sign_ofSubtype, Algebra.Norm.Transitivity.det_mul_corner_pow, Fintype.prod_eq_mul_prod_subtype_ne, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, char_dvd_card_solutions_of_fintype_sum_lt, NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, Fintype.prod_fiberwise, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply, SimpleGraph.card_edgeFinset_induce_compl_singleton, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm

(root)

Definitions

Name	Category	Theorems
finsetStx 📖	CompOp	—
precheckFinsetStx 📖	CompOp	—
setFintype 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_image_univ_iff_mem_range 📖	mathematical	—	Finset Finset.instMembership Finset.image Finset.univ Set Set.instMembership Set.range	—	—

---

← Back to Index