Basic

📁 Source: Mathlib/Combinatorics/Derangements/Basic.lean

Statistics

Metric	Count
Definitions derangementsCongr, derangements, fiber, atMostOneFixedPointEquivSum_derangements, derangementsOptionEquivSigmaAtMostOneFixedPoint, derangementsRecursionEquiv, subtypeEquiv	7
Theorems fiber_none, fiber_some, mem_fiber, mem_derangements_iff_fixedPoints_eq_empty	4
Total	11

Equiv

Definitions

Name	Category	Theorems
derangementsCongr 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
derangements 📖	CompOp	6 math math: mem_derangements_iff_fixedPoints_eq_empty, card_derangements_invariant, derangements.Equiv.RemoveNone.mem_fiber, card_derangements_fin_add_two, card_derangements_eq_numDerangements, card_derangements_fin_eq_numDerangements

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_derangements_iff_fixedPoints_eq_empty 📖	mathematical	—	Equiv.Perm Set Set.instMembership derangements Function.fixedPoints DFunLike.coe EquivLike.toFunLike Equiv.instEquivLike Set.instEmptyCollection	—	Set.eq_empty_iff_forall_notMem

derangements

Definitions

Name	Category	Theorems
atMostOneFixedPointEquivSum_derangements 📖	CompOp	—
derangementsOptionEquivSigmaAtMostOneFixedPoint 📖	CompOp	—
derangementsRecursionEquiv 📖	CompOp	—
subtypeEquiv 📖	CompOp	—

derangements.Equiv.RemoveNone

Definitions

Name	Category	Theorems
fiber 📖	CompOp	3 math math: mem_fiber, fiber_none, fiber_some

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fiber_none 📖	mathematical	—	fiber Set Equiv.Perm Set.instEmptyCollection	—	Set.eq_empty_iff_forall_notMem mem_fiber
fiber_some 📖	mathematical	—	fiber setOf Equiv.Perm Set Set.instHasSubset Function.fixedPoints DFunLike.coe EquivLike.toFunLike Equiv.instEquivLike Set.instSingletonSet	—	Set.ext mem_fiber Equiv.removeNone_none Function.mem_fixedPoints_iff Equiv.removeNone_some Equiv.swap_apply_left Equiv.swap_apply_right Equiv.swap_apply_self Option.some_injective Equiv.swap_apply_of_ne_of_ne Equiv.apply_symm_apply
mem_fiber 📖	mathematical	—	Equiv.Perm Set Set.instMembership fiber derangements DFunLike.coe EquivLike.toFunLike Equiv.instEquivLike Equiv.removeNone	—	Set.image_congr

---

← Back to Index