Documentation Verification Report

EquivFin

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

Statistics

Metric	Count
Definitions `embeddingEquivOfFinite`, `ofLeftInverseOfCardLE`, `ofRightInverseOfCardLE`, `equivFin`, `equivFinOfCardEq`, `equivOfCardEq`, `equivFin`, `equivFinOfCardEq`, `equivOfCardEq`, `ofFinite`, `truncEquivFin`, `truncEquivFinOfCardEq`, `truncEquivOfCardEq`, `truncFinBijection`, `equivOfFiniteSelfEmbedding`, `truncOfCardLE`, `natEmbedding`, `fintypeOfFinsetCardLe`, `fintypeOfNotInfinite`, `fintypeOrInfinite`	20
Theorems `embeddingEquivOfFinite_apply`, `embeddingEquivOfFinite_symm_apply`, `ofLeftInverseOfCardLE_apply`, `ofLeftInverseOfCardLE_symm_apply`, `ofRightInverseOfCardLE_apply`, `ofRightInverseOfCardLE_symm_apply`, `of_fintype`, `of_injective`, `of_subsingleton`, `of_surjective`, `card_eq_of_equiv`, `card_eq_of_equiv_fin`, `card_eq_of_equiv_fintype`, `univ_map_embedding`, `bijective_iff_injective_and_card`, `bijective_iff_surjective_and_card`, `card_eq`, `card_eq_one_iff`, `card_eq_one_iff_nonempty_unique`, `card_eq_one_of_forall_eq`, `card_le_one_iff`, `card_le_one_iff_subsingleton`, `card_lt_of_surjective_not_injective`, `exists_ne_of_one_lt_card`, `exists_pair_of_one_lt_card`, `false`, `finite`, `one_lt_card`, `one_lt_card_iff`, `one_lt_card_iff_nontrivial`, `exists_of_card_eq_finset`, `exists_of_card_le_finset`, `is_empty`, `nonempty_iff_card_le`, `nonempty_of_card_le`, `toEmbedding_equivOfFiniteSelfEmbedding`, `rightInverse_of_card_le`, `leftInverse_of_card_le`, `exists_notMem_finset`, `exists_subset_card_eq`, `exists_superset_card_eq`, `instNontrivial`, `instSigmaOfNonempty`, `instSigmaOfNonempty_1`, `nonempty`, `of_injective`, `of_injective_to_set`, `of_not_fintype`, `of_surjective`, `of_surjective_from_set`, `sigma_of_right`, `infinite`, `infinite_of_left`, `infinite_of_right`, `finite`, `finite`, `infinite`, `finite`, `infinite_of_left`, `infinite_of_right`, `finite_iff_nonempty_fintype`, `instFiniteProp`, `instInfiniteFinset`, `instInfiniteListOfNonempty`, `instInfiniteMultisetOfNonempty`, `instInfiniteNat`, `instInfiniteOption`, `instInfinitePerm`, `isEmpty_fintype`, `not_injective_infinite_finite`, `not_surjective_finite_infinite`	71
Total	91

Equiv

Definitions

Name	Category	Theorems
`embeddingEquivOfFinite` 📖	CompOp	2 math math: `embeddingEquivOfFinite_apply`, `embeddingEquivOfFinite_symm_apply`
`ofLeftInverseOfCardLE` 📖	CompOp	2 math math: `ofLeftInverseOfCardLE_apply`, `ofLeftInverseOfCardLE_symm_apply`
`ofRightInverseOfCardLE` 📖	CompOp	2 math math: `ofRightInverseOfCardLE_apply`, `ofRightInverseOfCardLE_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`embeddingEquivOfFinite_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Function.Embedding` `EquivLike.toFunLike` `instEquivLike` `embeddingEquivOfFinite` `Function.Embedding.equivOfFiniteSelfEmbedding`	—	—
`embeddingEquivOfFinite_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Function.Embedding` `EquivLike.toFunLike` `instEquivLike` `symm` `embeddingEquivOfFinite` `toEmbedding`	—	—
`ofLeftInverseOfCardLE_apply` 📖	mathematical	`Fintype.card`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `ofLeftInverseOfCardLE`	—	—
`ofLeftInverseOfCardLE_symm_apply` 📖	mathematical	`Fintype.card`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `ofLeftInverseOfCardLE`	—	—
`ofRightInverseOfCardLE_apply` 📖	mathematical	`Fintype.card`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `ofRightInverseOfCardLE`	—	—
`ofRightInverseOfCardLE_symm_apply` 📖	mathematical	`Fintype.card`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `ofRightInverseOfCardLE`	—	—

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_fintype` 📖	mathematical	—	`Finite`	—	`Fintype.finite`
`of_injective` 📖	mathematical	—	`Finite`	—	`exists_equiv_fin` `of_equiv` `of_fintype` `Equiv.injective`
`of_subsingleton` 📖	mathematical	—	`Finite`	—	`of_injective` `of_fintype` `Function.injective_of_subsingleton`
`of_surjective` 📖	mathematical	—	`Finite`	—	`of_injective` `Function.injective_surjInv`

Finset

Definitions

Name	Category	Theorems
`equivFin` 📖	CompOp	—
`equivFinOfCardEq` 📖	CompOp	—
`equivOfCardEq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_eq_of_equiv` 📖	mathematical	—	`card`	—	`card_eq_of_equiv_fintype` `Fintype.card_coe`
`card_eq_of_equiv_fin` 📖	mathematical	—	`card`	—	`Fin.equiv_iff_eq`
`card_eq_of_equiv_fintype` 📖	mathematical	—	`card` `Fintype.card`	—	`card_eq_of_equiv_fin`
`univ_map_embedding` 📖	mathematical	—	`map` `univ`	—	`Finite.of_fintype` `Function.Embedding.toEmbedding_equivOfFiniteSelfEmbedding` `univ_map_equiv_to_embedding`

Fintype

Definitions

Name	Category	Theorems
`equivFin` 📖	CompOp	6 math math: `CategoryTheory.FinCategory.categoryAsType_comp`, `CategoryTheory.FinCategory.asTypeToObjAsType_map`, `CategoryTheory.FinCategory.categoryAsType_id`, `CategoryTheory.FinCategory.asTypeToObjAsType_obj`, `CategoryTheory.FinCategory.objAsTypeToAsType_map`, `CategoryTheory.FinCategory.objAsTypeToAsType_obj`
`equivFinOfCardEq` 📖	CompOp	—
`equivOfCardEq` 📖	CompOp	—
`ofFinite` 📖	CompOp	8 math math: `CuspForm.coe_trace`, `PiTensorProduct.dualDistribEquivOfBasis_apply_apply`, `Nat.card_eq`, `SlashInvariantForm.coe_trace`, `ModularForm.coe_norm`, `Algebra.TensorProduct.equivPiOfFiniteBasis_symm_apply`, `ModularForm.coe_trace`, `SlashInvariantForm.coe_norm`
`truncEquivFin` 📖	CompOp	—
`truncEquivFinOfCardEq` 📖	CompOp	—
`truncEquivOfCardEq` 📖	CompOp	—
`truncFinBijection` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_iff_injective_and_card` 📖	mathematical	—	`Function.Bijective` `card`	—	`card_of_bijective` `Function.Injective.surjective_of_finite` `Finite.of_fintype`
`bijective_iff_surjective_and_card` 📖	mathematical	—	`Function.Bijective` `card`	—	`card_of_bijective` `Function.Surjective.injective_of_finite` `Finite.of_fintype`
`card_eq` 📖	mathematical	—	`card` `Equiv`	—	`Trunc.nonempty` `card_congr`
`card_eq_one_iff` 📖	mathematical	—	`card`	—	`card_unit` `card_eq` `Equiv.injective`
`card_eq_one_iff_nonempty_unique` 📖	mathematical	—	`card` `Unique`	—	`card_eq_one_iff` `card_unique`
`card_eq_one_of_forall_eq` 📖	mathematical	—	`card`	—	`card_eq_one_iff`
`card_le_one_iff` 📖	mathematical	—	`card`	—	`card_eq_zero_iff` `card_eq_one_iff` `le_rfl` `card_le_of_injective` `card_unit`
`card_le_one_iff_subsingleton` 📖	mathematical	—	`card`	—	`card_le_one_iff` `subsingleton_iff`
`card_lt_of_surjective_not_injective` 📖	mathematical	—	`card`	—	`card_lt_of_injective_not_surjective` `Function.injective_surjInv` `Function.Surjective.injective_of_finite` `Finite.of_fintype`
`exists_ne_of_one_lt_card` 📖	—	`card`	—	—	`exists_ne` `one_lt_card_iff_nontrivial`
`exists_pair_of_one_lt_card` 📖	—	`card`	—	—	`exists_pair_ne` `one_lt_card_iff_nontrivial`
`false` 📖	—	—	—	—	`not_finite` `Finite.of_fintype`
`finite` 📖	mathematical	—	`Finite`	—	—
`one_lt_card` 📖	mathematical	—	`card`	—	`one_lt_card_iff_nontrivial`
`one_lt_card_iff` 📖	mathematical	—	`card`	—	`one_lt_card_iff_nontrivial` `nontrivial_iff`
`one_lt_card_iff_nontrivial` 📖	mathematical	—	`card` `Nontrivial`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `card_le_one_iff_subsingleton`

Function.Embedding

Definitions

Name	Category	Theorems
`equivOfFiniteSelfEmbedding` 📖	CompOp	2 math math: `Equiv.embeddingEquivOfFinite_apply`, `toEmbedding_equivOfFiniteSelfEmbedding`
`truncOfCardLE` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_of_card_eq_finset` 📖	mathematical	`Fintype.card` `Finset.card`	`Finset.map` `Finset.univ`	—	`exists_of_card_le_finset` `Finset.eq_of_subset_of_card_le` `Finset.coe_map` `Finset.coe_univ` `Set.image_univ` `Finset.card_map`
`exists_of_card_le_finset` 📖	mathematical	`Fintype.card` `Finset.card`	`Set` `Set.instHasSubset` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`nonempty_of_card_le` `Fintype.card_coe`
`is_empty` 📖	mathematical	—	`IsEmpty` `Function.Embedding`	—	`not_injective_infinite_finite` `inj'`
`nonempty_iff_card_le` 📖	mathematical	—	`Function.Embedding` `Fintype.card`	—	`Fintype.card_le_of_embedding` `nonempty_of_card_le`
`nonempty_of_card_le` 📖	mathematical	`Fintype.card`	`Function.Embedding`	—	`Trunc.nonempty`
`toEmbedding_equivOfFiniteSelfEmbedding` 📖	mathematical	—	`Equiv.toEmbedding` `equivOfFiniteSelfEmbedding`	—	`ext`

Function.LeftInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rightInverse_of_card_le` 📖	—	`Fintype.card`	—	—	`Function.surjective_iff_hasRightInverse` `Fintype.bijective_iff_surjective_and_card` `le_antisymm` `Fintype.card_le_of_surjective`

Function.RightInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leftInverse_of_card_le` 📖	—	`Fintype.card`	—	—	`Function.LeftInverse.rightInverse_of_card_le`

Infinite

Definitions

Name	Category	Theorems
`natEmbedding` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_notMem_finset` 📖	mathematical	—	`Finset` `Finset.instMembership`	—	`Fintype.false`
`exists_subset_card_eq` 📖	mathematical	—	`Finset.card`	—	`Finset.card_map` `Finset.card_range`
`exists_superset_card_eq` 📖	mathematical	`Finset.card`	`Finset` `Finset.instHasSubset`	—	`subset_rfl` `Finset.instReflSubset` `LE.le.eq_or_lt` `exists_notMem_finset` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `Finset.subset_cons` `Finset.card_cons`
`instNontrivial` 📖	mathematical	—	`Nontrivial`	—	`exists_notMem_finset`
`instSigmaOfNonempty` 📖	mathematical	—	`Infinite`	—	`of_surjective` `Sigma.fst_surjective`
`instSigmaOfNonempty_1` 📖	—	`Infinite`	—	—	`sigma_of_right`
`nonempty` 📖	—	—	—	—	`Nontrivial.to_nonempty` `instNontrivial`
`of_injective` 📖	mathematical	—	`Infinite`	—	`Finite.false` `Finite.of_injective`
`of_injective_to_set` 📖	mathematical	`Set.Elem`	`Infinite`	—	`of_not_fintype` `lt_irrefl` `Fintype.card_le_of_injective` `Set.toFinset_card` `Finset.card_lt_card` `Set.toFinset_ssubset_univ` `Set.ssubset_univ_iff`
`of_not_fintype` 📖	mathematical	—	`Infinite`	—	`isEmpty_fintype`
`of_surjective` 📖	mathematical	—	`Infinite`	—	`Finite.false` `Finite.of_surjective`
`of_surjective_from_set` 📖	mathematical	`Set.Elem`	`Infinite`	—	`of_injective_to_set` `Function.injective_surjInv`
`sigma_of_right` 📖	mathematical	—	`Infinite`	—	`of_injective`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infinite` 📖	mathematical	—	`Infinite`	—	`Infinite.of_injective` `instInfiniteNat`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infinite_of_left` 📖	mathematical	—	`Infinite`	—	`Infinite.of_surjective` `fst_surjective`
`infinite_of_right` 📖	mathematical	—	`Infinite`	—	`Infinite.of_surjective` `snd_surjective`

Quot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Finite`	—	`Finite.of_surjective` `mk_surjective`

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Finite`	—	`Quot.finite`

String

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infinite` 📖	mathematical	—	`Infinite`	—	`Infinite.of_injective` `instInfiniteListOfNonempty`

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Finite`	—	`Finite.of_injective` `coe_injective`

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infinite_of_left` 📖	mathematical	—	`Infinite`	—	`Infinite.of_injective` `inl_injective`
`infinite_of_right` 📖	mathematical	—	`Infinite`	—	`Infinite.of_injective` `inr_injective`

(root)

Definitions

Name	Category	Theorems
`fintypeOfFinsetCardLe` 📖	CompOp	—
`fintypeOfNotInfinite` 📖	CompOp	—
`fintypeOrInfinite` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_iff_nonempty_fintype` 📖	mathematical	—	`Finite` `Fintype`	—	`nonempty_fintype` `Finite.of_fintype`
`instFiniteProp` 📖	mathematical	—	`Finite`	—	`Finite.of_subsingleton`
`instInfiniteFinset` 📖	mathematical	—	`Infinite` `Finset`	—	`Infinite.of_injective` `Finset.singleton_injective`
`instInfiniteListOfNonempty` 📖	mathematical	—	`Infinite`	—	`Infinite.of_surjective` `instInfiniteMultisetOfNonempty` `Quot.mk_surjective`
`instInfiniteMultisetOfNonempty` 📖	mathematical	—	`Infinite` `Multiset`	—	`Infinite.of_injective` `instInfiniteNat` `Multiset.replicate_left_injective`
`instInfiniteNat` 📖	mathematical	—	`Infinite`	—	`Infinite.of_not_fintype` `LE.le.not_gt` `Finset.card_le_univ` `LT.lt.trans_eq` `Finset.card_range`
`instInfiniteOption` 📖	mathematical	—	`Infinite`	—	`Infinite.of_injective` `Option.some_injective`
`instInfinitePerm` 📖	mathematical	—	`Infinite` `Equiv.Perm`	—	`Nontrivial.to_nonempty` `Infinite.instNontrivial` `Infinite.of_injective` `Equiv.swap_injective_of_left`
`isEmpty_fintype` 📖	mathematical	—	`IsEmpty` `Fintype` `Infinite`	—	`nonempty_fintype` `Fintype.finite`
`not_injective_infinite_finite` 📖	—	—	—	—	`Finite.false` `Finite.of_injective`
`not_surjective_finite_infinite` 📖	—	—	—	—	`Infinite.not_finite` `Infinite.of_surjective`

---

← Back to Index