Theorems · Theorem · order theory
Finset.map_univ_equiv
∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (f : β ≃ α),
Finset.map f.toEmbedding Finset.univ = Finset.univ- Defined in
- Mathlib.Data.Finset.BooleanAlgebra
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Equivstatement and proof · cited by 8,337
- Fintypestatement and proof · cited by 7,736
- Finset.univstatement · cited by 3,473
- Finset.mapstatement · cited by 747
- Equiv.toEmbeddingstatement · cited by 254
- Equiv.surjectiveproof · cited by 198
- Finset.map_univ_of_surjectiveproof · cited by 2
Cited by12
Results whose statement or proof uses this declaration.
- Affine.Simplex.exsphere_reindexproof · cited by 5
- Function.Odd.sum_eq_zeroproof · cited by 3
- Multiset.map_univ_val_equivproof · cited by 2
- MvPolynomial.rename_esymmproof · cited by 2
- Affine.Simplex.setInterior_reindexproof · cited by 2
- Affine.Simplex.excenterWeights_reindexproof · cited by 1
- MultilinearMap.domCoprod_alternizationproof · cited by 1
- MonoidHom.card_fiber_eq_of_mem_rangeproof · cited by 1
- Multiset.bijective_iff_map_univ_eq_univproof · cited by 0
- Affine.Simplex.touchpointWeights_reindexproof · cited by 0
- AddMonoidHom.card_fiber_eq_of_mem_rangeproof · cited by 0
- Affine.Simplex.excenterExists_reindexproof · cited by 0