Rev

Statistics

Metric	Count
Definitions `revPerm`	1
Theorems `add_rev_cast`, `cast_rev`, `le_rev_iff`, `lt_rev_iff`, `predAbove_rev_left`, `predAbove_rev_right`, `revPerm_apply`, `revPerm_symm`, `revPerm_symm_apply`, `rev_add_cast`, `rev_bijective`, `rev_castPred`, `rev_eq_iff`, `rev_injective`, `rev_involutive`, `rev_le_iff`, `rev_lt_iff`, `rev_ne_iff`, `rev_pred`, `rev_predAbove`, `rev_succAbove`, `rev_surjective`, `succAbove_rev_left`, `succAbove_rev_right`, `val_rev_zero`	25
Total	26

Fin

Definitions

Name	Category	Theorems
`revPerm` 📖	CompOp	17 math math: `map_revPerm_Ioc`, `revPerm_symm`, `map_revPerm_Ico`, `isSymmSndFDerivAt_iff_iteratedFDeriv`, `map_revPerm_Ici`, `map_revPerm_Icc`, `map_revPerm_Ioi`, `revOrderIso_toEquiv`, `revPerm_apply`, `map_revPerm_Ioo`, `map_revPerm_uIcc`, `map_revPerm_Iio`, `LinearMap.IsSymmetric.eigenvalues_def`, `isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin`, `revPerm_symm_apply`, `map_revPerm_Iic`, `LinearMap.IsSymmetric.eigenvectorBasis_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_rev_cast` 📖	—	—	—	—	—
`cast_rev` 📖	—	—	—	—	—
`le_rev_iff` 📖	—	—	—	—	—
`lt_rev_iff` 📖	—	—	—	—	—
`predAbove_rev_left` 📖	mathematical	—	`predAbove`	—	`succ_le_or_le_castSucc` `predAbove_of_succ_le` `rev_ne_iff` `rev_pred` `le_rev_iff` `predAbove_of_le_castSucc` `rev_castPred` `rev_le_iff`
`predAbove_rev_right` 📖	mathematical	—	`predAbove`	—	`predAbove_rev_left`
`revPerm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `revPerm`	—	—
`revPerm_symm` 📖	mathematical	—	`Equiv.symm` `revPerm`	—	—
`revPerm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `revPerm`	—	—
`rev_add_cast` 📖	—	—	—	—	`add_rev_cast`
`rev_bijective` 📖	mathematical	—	`Function.Bijective`	—	`Function.Involutive.bijective` `rev_involutive`
`rev_castPred` 📖	mathematical	`rev_ne_iff`	`castPred`	—	`castSucc_castPred`
`rev_eq_iff` 📖	—	—	—	—	—
`rev_injective` 📖	—	—	—	—	`Function.Involutive.injective` `rev_involutive`
`rev_involutive` 📖	mathematical	—	`Function.Involutive`	—	—
`rev_le_iff` 📖	—	—	—	—	—
`rev_lt_iff` 📖	—	—	—	—	—
`rev_ne_iff` 📖	—	—	—	—	`Iff.not` `rev_eq_iff`
`rev_pred` 📖	mathematical	`rev_ne_iff`	`castPred`	—	`castSucc_castPred`
`rev_predAbove` 📖	mathematical	—	`predAbove`	—	`predAbove_rev_left`
`rev_succAbove` 📖	mathematical	—	`succAbove`	—	`succAbove_rev_left`
`rev_surjective` 📖	—	—	—	—	`Function.Involutive.surjective` `rev_involutive`
`succAbove_rev_left` 📖	mathematical	—	`succAbove`	—	`succ_le_or_le_castSucc` `succAbove_of_succ_le` `succAbove_of_le_castSucc` `le_rev_iff` `rev_le_iff`
`succAbove_rev_right` 📖	mathematical	—	`succAbove`	—	`succAbove_rev_left`
`val_rev_zero` 📖	—	—	—	—	—

---

← Back to Index