ClosureSwap

📁 Source: Mathlib/GroupTheory/Perm/ClosureSwap.lean

Statistics

Metric	Count
Definitions	0
Theorems finite_compl_fixedBy, swap_mem_trans, closure_of_isSwap_of_isPretransitive, exists_smul_notMem_of_subset_orbit_closure, finite_compl_fixedBy_closure_iff, finite_compl_fixedBy_swap, mem_closure_isSwap, mem_closure_isSwap', surjective_of_isSwap_of_isPretransitive, surjective_of_isSwap_of_isPretransitive', swap_mem_closure_isSwap	11
Total	11

Equiv.Perm.IsSwap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_compl_fixedBy 📖	mathematical	Equiv.Perm.IsSwap	Set.Finite Compl.compl Set Set.instCompl MulAction.fixedBy Equiv.Perm DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Equiv.Perm.applyMulAction	—	finite_compl_fixedBy_swap

SubmonoidClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
swap_mem_trans 📖	mathematical	Equiv.Perm SetLike.instMembership Equiv.swap	Equiv.Perm SetLike.instMembership Equiv.swap	—	eq_or_ne OneMemClass.one_mem toOneMemClass Equiv.swap_self Equiv.swap_comm Equiv.swap_mul_swap_mul_swap MulMemClass.mul_mem toMulMemClass

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_of_isSwap_of_isPretransitive 📖	mathematical	Equiv.Perm.IsSwap	Subgroup.closure Equiv.Perm Equiv.Perm.permGroup Top.top Subgroup Subgroup.instTop	—	mem_closure_isSwap Subtype.finite MulAction.orbit_eq_univ
exists_smul_notMem_of_subset_orbit_closure 📖	mathematical	Set Set.instMembership InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set.instHasSubset MulAction.orbit Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.closure SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction MulAction.instMulAction Set.Nonempty	Set Set.instMembership SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	Mathlib.Tactic.Contrapose.contrapose₄ Set.smul_mem_smul_set_iff Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq Subgroup.closure_le smul_inv_smul
finite_compl_fixedBy_closure_iff 📖	mathematical	—	Set.Finite Compl.compl Set Set.instCompl MulAction.fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Subgroup.subset_closure Subgroup.closure_induction MulAction.fixedBy_one_eq_univ Set.compl_univ Set.Finite.subset Set.Finite.union MulAction.fixedBy_inv
finite_compl_fixedBy_swap 📖	mathematical	—	Set.Finite Compl.compl Set Set.instCompl MulAction.fixedBy Equiv.Perm DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Equiv.Perm.applyMulAction Equiv.swap	—	Set.Finite.subset Set.compl_subset_comm Equiv.swap_apply_of_ne_of_ne
mem_closure_isSwap 📖	mathematical	Equiv.Perm.IsSwap	Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike Subgroup.closure Set.Finite Compl.compl Set Set.instCompl MulAction.fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.applyMulAction Set.instMembership MulAction.orbit SemigroupAction.toSMul Monoid.toSemigroup Subgroup.toGroup MulAction.toSemigroupAction MulAction.instMulAction DFunLike.coe EquivLike.toFunLike Equiv.instEquivLike	—	finite_compl_fixedBy_closure_iff Equiv.Perm.IsSwap.finite_compl_fixedBy MulAction.mem_orbit_iff Set.Finite.induction_on Equiv.Perm.ext Subgroup.one_mem mul_mem_cancel_left Subgroup.instSubgroupClass swap_mem_closure_isSwap Equiv.Perm.mul_apply Equiv.swap_apply_def MulAction.orbit_eq_iff MulAction.mem_orbit_self Mathlib.Tactic.Contrapose.contrapose₁ Eq.subset Set.instReflSubset
mem_closure_isSwap' 📖	mathematical	—	Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike Subgroup.closure setOf Equiv.Perm.IsSwap Set.Finite Compl.compl Set Set.instCompl MulAction.fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.applyMulAction	—	mem_closure_isSwap Equiv.swap_self Subgroup.one_mem Subgroup.subset_closure Equiv.swap_apply_left
surjective_of_isSwap_of_isPretransitive 📖	mathematical	Equiv.Perm.IsSwap DFunLike.coe MonoidHom Equiv.Perm MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup MonoidHom.instFunLike MulAction.toPermHom Subgroup.closure Top.top Subgroup Subgroup.instTop	Equiv.Perm DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup MonoidHom.instFunLike MulAction.toPermHom	—	surjective_of_isSwap_of_isPretransitive'
surjective_of_isSwap_of_isPretransitive' 📖	mathematical	DFunLike.coe MonoidHom Equiv.Perm MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup MonoidHom.instFunLike MulAction.toPermHom Equiv.Perm.instOne Equiv.Perm.IsSwap Subgroup.closure Top.top Subgroup Subgroup.instTop	Equiv.Perm DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup MonoidHom.instFunLike MulAction.toPermHom	—	Subgroup.closure_diff_one MonoidHom.map_closure MonoidHom.range_eq_map MulAction.IsPretransitive.of_compHom MonoidHom.range_eq_top closure_of_isSwap_of_isPretransitive
swap_mem_closure_isSwap 📖	mathematical	Equiv.Perm.IsSwap	Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike Subgroup.closure Equiv.swap Set Set.instMembership MulAction.orbit SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction MulAction.instMulAction Equiv.Perm.applyMulAction	—	Equiv.swap_apply_right exists_smul_notMem_of_subset_orbit_closure Equiv.swap_inv MulAction.orbit_eq_iff Set.mem_setOf Equiv.swap_self OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass SubmonoidClass.swap_mem_trans Equiv.swap_apply_ne_self_iff Equiv.Perm.smul_def Equiv.swap_apply_left Equiv.swap_comm Subgroup.subset_closure

---

← Back to Index