Documentation Verification Report

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` 📖	—	`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` 📖	—	`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`	—	—	`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` 📖	—	`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`	—	—	`surjective_of_isSwap_of_isPretransitive'`
`surjective_of_isSwap_of_isPretransitive'` 📖	—	`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`	—	—	`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