Inv

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

Statistics

Metric	Count
Definitions bijInv, chooseX, invOfMemRange, invOfMemRange	4
Theorems bijective_bijInv, choose_spec, choose_subtype_eq, leftInverse_bijInv, rightInverse_bijInv, invFun_restrict, invOfMemRange_surjective, left_inv_of_invOfMemRange, right_inv_of_invOfMemRange, invFun_restrict, invOfMemRange_surjective, left_inv_of_invOfMemRange, right_inv_of_invOfMemRange	13
Total	17

Fintype

Definitions

Name	Category	Theorems
bijInv 📖	CompOp	3 math math: bijective_bijInv, leftInverse_bijInv, rightInverse_bijInv
chooseX 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_bijInv 📖	mathematical	Function.Bijective	bijInv	—	Function.RightInverse.injective rightInverse_bijInv Function.LeftInverse.surjective leftInverse_bijInv
choose_spec 📖	mathematical	ExistsUnique	choose	—	—
choose_subtype_eq 📖	mathematical	ExistsUnique	choose	—	choose_spec
leftInverse_bijInv 📖	mathematical	Function.Bijective	bijInv	—	choose_spec Function.Bijective.existsUnique
rightInverse_bijInv 📖	mathematical	Function.Bijective	bijInv	—	choose_spec Function.Bijective.existsUnique

Function.Embedding

Definitions

Name	Category	Theorems
invOfMemRange 📖	CompOp	5 math math: right_inv_of_invOfMemRange, invFun_restrict, invOfMemRange_surjective, Equiv.Perm.viaFintypeEmbedding_apply_mem_range, left_inv_of_invOfMemRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invFun_restrict 📖	mathematical	—	Set.restrict Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding Function.invFun invOfMemRange	—	injective Function.invFun_eq Set.mem_range left_inv_of_invOfMemRange
invOfMemRange_surjective 📖	mathematical	—	Set.Elem Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding invOfMemRange	—	Set.mem_range_self right_inv_of_invOfMemRange
left_inv_of_invOfMemRange 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding invOfMemRange Set Set.instMembership Set.range	—	Function.Injective.left_inv_of_invOfMemRange injective
right_inv_of_invOfMemRange 📖	mathematical	—	invOfMemRange Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding Set.mem_range_self	—	Function.Injective.right_inv_of_invOfMemRange injective

Function.Injective

Definitions

Name	Category	Theorems
invOfMemRange 📖	CompOp	4 math math: right_inv_of_invOfMemRange, left_inv_of_invOfMemRange, invFun_restrict, invOfMemRange_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invFun_restrict 📖	mathematical	—	Set.restrict Set.range Function.invFun invOfMemRange	—	Function.invFun_eq Set.mem_range left_inv_of_invOfMemRange
invOfMemRange_surjective 📖	mathematical	—	Set.Elem Set.range invOfMemRange	—	Set.mem_range_self right_inv_of_invOfMemRange
left_inv_of_invOfMemRange 📖	mathematical	—	invOfMemRange Set Set.instMembership Set.range	—	Finset.choose_spec
right_inv_of_invOfMemRange 📖	mathematical	—	invOfMemRange Set Set.instMembership Set.range Set.mem_range_self	—	Set.mem_range_self Finset.choose_spec

---

← Back to Index