Equidecomp

📁 Source: Mathlib/Algebra/Group/Action/Equidecomp.lean

Statistics

Metric	Count
Definitions Equidecomp, IsDecompOn, instCoeFunForall, refl, restr, toPartialEquiv, trans, witness	8
Theorems comp, comp', mono, of_leftInvOn, apply_mem_target, isDecompOn, isDecompOn', left_inv, map_target, refl_symm, refl_toPartialEquiv, restr_invFun, restr_of_source_subset, restr_refl_symm, restr_source, restr_target, restr_toFun, restr_univ, right_inv, source_restr, symm_bijective, symm_involutive, symm_symm, symm_toPartialEquiv, toPartialEquiv_injective, toPartialEquiv_restr, trans_toPartialEquiv	27
Total	35

Equidecomp

Definitions

Name	Category	Theorems
IsDecompOn 📖	MathDef	6 math math: IsDecompOn.comp, isDecompOn', IsDecompOn.of_leftInvOn, isDecompOn, IsDecompOn.comp', IsDecompOn.mono
instCoeFunForall 📖	CompOp	—
refl 📖	CompOp	3 math math: restr_refl_symm, refl_toPartialEquiv, refl_symm
restr 📖	CompOp	9 math math: restr_invFun, source_restr, restr_refl_symm, restr_univ, toPartialEquiv_restr, restr_of_source_subset, restr_toFun, restr_source, restr_target
toPartialEquiv 📖	CompOp	16 math math: restr_invFun, map_target, source_restr, isDecompOn', left_inv, refl_toPartialEquiv, right_inv, toPartialEquiv_injective, isDecompOn, toPartialEquiv_restr, apply_mem_target, restr_toFun, restr_source, trans_toPartialEquiv, symm_toPartialEquiv, restr_target
trans 📖	CompOp	1 math math: trans_toPartialEquiv
witness 📖	CompOp	1 math math: isDecompOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_mem_target 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	Set Set.instMembership PartialEquiv.target toPartialEquiv PartialEquiv.toFun	—	—
isDecompOn 📖	mathematical	—	IsDecompOn PartialEquiv.toFun toPartialEquiv PartialEquiv.source witness	—	isDecompOn'
isDecompOn' 📖	mathematical	—	Finset IsDecompOn PartialEquiv.toFun toPartialEquiv PartialEquiv.source	—	—
left_inv 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	PartialEquiv.toFun PartialEquiv.symm toPartialEquiv SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	PartialEquiv.left_inv
map_target 📖	mathematical	Set Set.instMembership PartialEquiv.target toPartialEquiv SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	Set Set.instMembership PartialEquiv.source toPartialEquiv SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction PartialEquiv.toFun symm	—	PartialEquiv.map_target
refl_symm 📖	mathematical	—	symm refl DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
refl_toPartialEquiv 📖	mathematical	—	toPartialEquiv SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction refl PartialEquiv.refl	—	—
restr_invFun 📖	mathematical	—	PartialEquiv.invFun toPartialEquiv restr PartialEquiv.toFun PartialEquiv.symm	—	—
restr_of_source_subset 📖	mathematical	Set Set.instHasSubset PartialEquiv.source toPartialEquiv	restr	—	toPartialEquiv_injective toPartialEquiv_restr PartialEquiv.restr_eq_of_source_subset
restr_refl_symm 📖	mathematical	—	symm restr SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction refl	—	—
restr_source 📖	mathematical	—	PartialEquiv.source toPartialEquiv restr Set Set.instInter	—	—
restr_target 📖	mathematical	—	PartialEquiv.target toPartialEquiv restr Set Set.instInter Set.preimage PartialEquiv.toFun PartialEquiv.symm	—	—
restr_toFun 📖	mathematical	—	PartialEquiv.toFun toPartialEquiv restr	—	—
restr_univ 📖	mathematical	—	restr Set.univ	—	restr_of_source_subset Set.subset_univ
right_inv 📖	mathematical	Set Set.instMembership PartialEquiv.target toPartialEquiv SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	PartialEquiv.toFun toPartialEquiv SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction PartialEquiv.symm	—	PartialEquiv.right_inv
source_restr 📖	mathematical	Set Set.instHasSubset PartialEquiv.source toPartialEquiv	PartialEquiv.source toPartialEquiv restr	—	restr_source Set.inter_eq_self_of_subset_right
symm_bijective 📖	mathematical	—	Function.Bijective Equidecomp SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction symm	—	Function.Involutive.bijective symm_involutive
symm_involutive 📖	mathematical	—	Function.Involutive Equidecomp SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction symm	—	symm_symm
symm_symm 📖	mathematical	—	symm	—	—
symm_toPartialEquiv 📖	mathematical	—	toPartialEquiv SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction symm PartialEquiv.symm	—	—
toPartialEquiv_injective 📖	mathematical	—	Equidecomp PartialEquiv toPartialEquiv	—	—
toPartialEquiv_restr 📖	mathematical	—	toPartialEquiv restr PartialEquiv.restr	—	—
trans_toPartialEquiv 📖	mathematical	—	toPartialEquiv SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction trans PartialEquiv.trans	—	—

Equidecomp.IsDecompOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	Equidecomp.IsDecompOn SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Set.MapsTo	Equidecomp.IsDecompOn SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Finset Finset.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	Set.left_eq_inter comp'
comp' 📖	mathematical	Equidecomp.IsDecompOn SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	Equidecomp.IsDecompOn SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Set Set.instInter Set.preimage Finset Finset.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	Finset.mul_mem_mul SemigroupAction.mul_smul
mono 📖	mathematical	Equidecomp.IsDecompOn Set Set.instHasSubset Set.EqOn	Equidecomp.IsDecompOn	—	—
of_leftInvOn 📖	mathematical	Equidecomp.IsDecompOn SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Set.LeftInvOn	Equidecomp.IsDecompOn SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Set.image Finset Finset.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Finset.inv_mem_inv inv_smul_smul

(root)

Definitions

Name	Category	Theorems
Equidecomp 📖	CompData	3 math math: Equidecomp.toPartialEquiv_injective, Equidecomp.symm_involutive, Equidecomp.symm_bijective

---

← Back to Index