Theorems · Theorem · combinatorics
Equiv.finite_iff
∀ {α : Sort u_1} {β : Sort u_2} (f : α ≃ β), Finite α ↔ Finite β- Defined in
- Mathlib.Data.Finite.Defs
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement and proof · cited by 8,337
- Equiv.symmproof · cited by 3,681
- Finitestatement and proof · cited by 3,029
- Finite.of_equivproof · cited by 20
Cited by21
Results whose statement or proof uses this declaration.
- Set.finite_univ_iffproof · cited by 10
- Algebra.QuasiFinite.iff_finite_comap_preimage_singletonproof · cited by 4
- Algebra.QuasiFinite.finite_comap_preimage_singletonproof · cited by 3
- AddSubgroup.IsComplement.finite_left_iffproof · cited by 3
- Subgroup.IsComplement.finite_left_iffproof · cited by 3
- Topology.RelCWComplex.finite_cells_of_finiteproof · cited by 2
- AlgebraicGeometry.IsAffineOpen.iSup_of_disjointproof · cited by 2
- finite_iff_addSubgroup_quotientproof · cited by 2
- Equiv.infinite_iffproof · cited by 2
- Function.Bijective.finite_iffproof · cited by 1
- Equiv.set_finite_iffproof · cited by 1