PEquiv

Statistics

Metric	Count
Definitions `toPEquiv`, `PEquiv`, `instBotPEquiv`, `instFunLikeOption`, `instInhabited`, `instOrderBot`, `instPartialOrderPEquiv`, `instSemilatticeInfOfDecidableEq`, `invFun`, `ofSet`, `refl`, `single`, `toFun`, `trans`, `_»`	15
Theorems `toPEquiv_apply`, `toPEquiv_refl`, `toPEquiv_symm`, `toPEquiv_trans`, `bot_apply`, `bot_trans`, `coe_mk`, `coe_mk_apply`, `eq_some_iff`, `ext`, `ext_iff`, `inj`, `injective_of_forall_isSome`, `injective_of_forall_ne_isSome`, `inv`, `isSome_symm_get`, `le_def`, `mem_iff_mem`, `mem_ofSet_iff`, `mem_ofSet_self_iff`, `mem_single`, `mem_single_iff`, `mem_trans`, `ofSet_eq_refl`, `ofSet_eq_some_iff`, `ofSet_eq_some_self_iff`, `ofSet_symm`, `ofSet_univ`, `refl_apply`, `refl_trans`, `self_trans_symm`, `single_apply`, `single_apply_of_ne`, `single_subsingleton_eq_refl`, `single_trans_of_eq_none`, `single_trans_of_mem`, `single_trans_single`, `single_trans_single_of_ne`, `symm_bijective`, `symm_bot`, `symm_injective`, `symm_refl`, `symm_single`, `symm_symm`, `symm_trans_rev`, `symm_trans_self`, `trans_assoc`, `trans_bot`, `trans_eq_none`, `trans_eq_some`, `trans_refl`, `trans_single_of_eq_none`, `trans_single_of_mem`, `trans_symm_eq_iff_forall_isSome`	54
Total	69

Equiv

Definitions

Name	Category	Theorems
`toPEquiv` 📖	CompOp	12 math math: `PEquiv.vecMul_toMatrix_toPEquiv`, `toPEquiv_apply`, `PEquiv.toMatrix_toPEquiv_mulVec`, `PEquiv.toMatrix_toPEquiv_eq`, `toPEquiv_symm`, `PEquiv.toMatrix_toPEquiv_mul`, `toPEquiv_refl`, `PEquiv.transpose_toMatrix_toPEquiv_apply`, `toPEquiv_trans`, `PEquiv.mul_toMatrix_toPEquiv`, `PEquiv.toMatrix_toPEquiv_apply`, `PEquiv.toMatrix_swap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `PEquiv.instFunLikeOption` `toPEquiv` `Equiv` `EquivLike.toFunLike` `instEquivLike`	—	—
`toPEquiv_refl` 📖	mathematical	—	`toPEquiv` `refl` `PEquiv.refl`	—	—
`toPEquiv_symm` 📖	mathematical	—	`toPEquiv` `symm` `PEquiv.symm`	—	—
`toPEquiv_trans` 📖	mathematical	—	`toPEquiv` `trans` `PEquiv.trans`	—	—

PEquiv

Definitions

Name	Category	Theorems
`instBotPEquiv` 📖	CompOp	8 math math: `single_trans_of_eq_none`, `toMatrix_bot`, `single_trans_single_of_ne`, `trans_single_of_eq_none`, `symm_bot`, `bot_trans`, `trans_bot`, `bot_apply`
`instFunLikeOption` 📖	CompOp	26 math math: `Equiv.toPEquiv_apply`, `mem_iff_mem`, `single_apply_of_ne`, `trans_symm_eq_iff_forall_isSome`, `mul_toMatrix_apply`, `trans_eq_some`, `ofSet_eq_some_iff`, `trans_eq_none`, `coe_mk`, `symm_trans_self`, `coe_mk_apply`, `refl_apply`, `ofSet_eq_some_self_iff`, `ext_iff`, `mem_trans`, `mem_ofSet_self_iff`, `eq_some_iff`, `single_apply`, `mem_single`, `mem_ofSet_iff`, `toMatrix_apply`, `toMatrix_mul_apply`, `le_def`, `self_trans_symm`, `mem_single_iff`, `bot_apply`
`instInhabited` 📖	CompOp	—
`instOrderBot` 📖	CompOp	—
`instPartialOrderPEquiv` 📖	CompOp	1 math math: `le_def`
`instSemilatticeInfOfDecidableEq` 📖	CompOp	—
`invFun` 📖	CompOp	1 math math: `inv`
`ofSet` 📖	CompOp	9 math math: `ofSet_symm`, `ofSet_eq_some_iff`, `symm_trans_self`, `ofSet_eq_some_self_iff`, `mem_ofSet_self_iff`, `mem_ofSet_iff`, `ofSet_univ`, `self_trans_symm`, `ofSet_eq_refl`
`refl` 📖	CompOp	10 math math: `trans_symm_eq_iff_forall_isSome`, `trans_refl`, `Equiv.toPEquiv_refl`, `symm_refl`, `refl_apply`, `single_subsingleton_eq_refl`, `refl_trans`, `toMatrix_refl`, `ofSet_univ`, `ofSet_eq_refl`
`single` 📖	CompOp	16 math math: `single_mul_single_of_ne`, `single_trans_of_eq_none`, `single_apply_of_ne`, `symm_single`, `single_trans_single_of_ne`, `single_mul_single_right`, `trans_single_of_mem`, `single_subsingleton_eq_refl`, `single_trans_single`, `trans_single_of_eq_none`, `single_apply`, `mem_single`, `mem_single_iff`, `toMatrix_swap`, `single_trans_of_mem`, `single_mul_single`
`toFun` 📖	CompOp	1 math math: `inv`
`trans` 📖	CompOp	20 math math: `single_trans_of_eq_none`, `trans_symm_eq_iff_forall_isSome`, `trans_eq_some`, `trans_refl`, `trans_eq_none`, `symm_trans_self`, `single_trans_single_of_ne`, `mem_trans`, `trans_single_of_mem`, `single_trans_single`, `trans_single_of_eq_none`, `refl_trans`, `symm_trans_rev`, `bot_trans`, `self_trans_symm`, `Equiv.toPEquiv_trans`, `toMatrix_trans`, `trans_bot`, `single_trans_of_mem`, `trans_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_apply` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `Bot.bot` `instBotPEquiv`	—	—
`bot_trans` 📖	mathematical	—	`trans` `Bot.bot` `PEquiv` `instBotPEquiv`	—	`ext`
`coe_mk` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption`	—	—
`coe_mk_apply` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption`	—	—
`eq_some_iff` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `symm`	—	`inv`
`ext` 📖	—	`DFunLike.coe` `PEquiv` `instFunLikeOption`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption`	—	`ext`
`inj` 📖	—	`DFunLike.coe` `PEquiv` `instFunLikeOption`	—	—	`mem_iff_mem`
`injective_of_forall_isSome` 📖	—	`DFunLike.coe` `PEquiv` `instFunLikeOption`	—	—	`injective_of_forall_ne_isSome`
`injective_of_forall_ne_isSome` 📖	—	`DFunLike.coe` `PEquiv` `instFunLikeOption`	—	—	`not_imp_comm` `eq_some_iff`
`inv` 📖	mathematical	—	`invFun` `toFun`	—	—
`isSome_symm_get` 📖	mathematical	`DFunLike.coe` `PEquiv` `instFunLikeOption`	`symm`	—	`eq_some_iff`
`le_def` 📖	mathematical	—	`PEquiv` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderPEquiv` `DFunLike.coe` `instFunLikeOption`	—	—
`mem_iff_mem` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `symm`	—	`inv`
`mem_ofSet_iff` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `ofSet` `Set` `Set.instMembership`	—	—
`mem_ofSet_self_iff` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `ofSet` `Set` `Set.instMembership`	—	—
`mem_single` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `single`	—	—
`mem_single_iff` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `single`	—	—
`mem_trans` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `trans`	—	—
`ofSet_eq_refl` 📖	mathematical	—	`ofSet` `refl` `Set.univ`	—	`Set.eq_univ_iff_forall` `mem_ofSet_self_iff` `ofSet.congr_simp`
`ofSet_eq_some_iff` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `ofSet` `Set` `Set.instMembership`	—	`mem_ofSet_iff`
`ofSet_eq_some_self_iff` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `ofSet` `Set` `Set.instMembership`	—	`mem_ofSet_self_iff`
`ofSet_symm` 📖	mathematical	—	`symm` `ofSet`	—	—
`ofSet_univ` 📖	mathematical	—	`ofSet` `Set.univ` `Set.decidableUniv` `refl`	—	—
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `refl`	—	—
`refl_trans` 📖	mathematical	—	`trans` `refl`	—	`ext`
`self_trans_symm` 📖	mathematical	—	`trans` `symm` `ofSet` `setOf` `DFunLike.coe` `PEquiv` `instFunLikeOption` `Set.decidableSetOf`	—	`ext` `eq_some_iff`
`single_apply` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `single`	—	—
`single_apply_of_ne` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `single`	—	—
`single_subsingleton_eq_refl` 📖	mathematical	—	`single` `refl`	—	`ext`
`single_trans_of_eq_none` 📖	mathematical	`DFunLike.coe` `PEquiv` `instFunLikeOption`	`trans` `single` `Bot.bot` `instBotPEquiv`	—	`symm_injective` `trans_single_of_eq_none`
`single_trans_of_mem` 📖	mathematical	`DFunLike.coe` `PEquiv` `instFunLikeOption`	`trans` `single`	—	`ext` `Option.bind_congr'`
`single_trans_single` 📖	mathematical	—	`trans` `single`	—	`single_trans_of_mem` `mem_single`
`single_trans_single_of_ne` 📖	mathematical	—	`trans` `single` `Bot.bot` `PEquiv` `instBotPEquiv`	—	`single_trans_of_eq_none` `single_apply_of_ne`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `PEquiv` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_bot` 📖	mathematical	—	`symm` `Bot.bot` `PEquiv` `instBotPEquiv`	—	—
`symm_injective` 📖	mathematical	—	`PEquiv` `symm`	—	`Function.Bijective.injective` `symm_bijective`
`symm_refl` 📖	mathematical	—	`symm` `refl`	—	—
`symm_single` 📖	mathematical	—	`symm` `single`	—	—
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_trans_rev` 📖	mathematical	—	`symm` `trans`	—	—
`symm_trans_self` 📖	mathematical	—	`trans` `symm` `ofSet` `setOf` `DFunLike.coe` `PEquiv` `instFunLikeOption` `Set.decidableSetOf`	—	`symm_injective` `self_trans_symm`
`trans_assoc` 📖	mathematical	—	`trans`	—	`ext`
`trans_bot` 📖	mathematical	—	`trans` `Bot.bot` `PEquiv` `instBotPEquiv`	—	`ext` `Option.bind_congr'`
`trans_eq_none` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `trans`	—	`imp_iff_not_or` `Mathlib.Tactic.Push.not_and_eq` `forall_swap`
`trans_eq_some` 📖	mathematical	—	`DFunLike.coe` `PEquiv` `instFunLikeOption` `trans`	—	—
`trans_refl` 📖	mathematical	—	`trans` `refl`	—	`ext` `Option.bind_congr'`
`trans_single_of_eq_none` 📖	mathematical	`DFunLike.coe` `PEquiv` `instFunLikeOption` `symm`	`trans` `single` `Bot.bot` `instBotPEquiv`	—	`ext` `eq_some_iff`
`trans_single_of_mem` 📖	mathematical	`DFunLike.coe` `PEquiv` `instFunLikeOption`	`trans` `single`	—	`symm_injective` `single_trans_of_mem` `mem_iff_mem`
`trans_symm_eq_iff_forall_isSome` 📖	mathematical	—	`trans` `symm` `refl` `DFunLike.coe` `PEquiv` `instFunLikeOption`	—	`self_trans_symm` `ofSet_eq_refl` `Set.eq_univ_iff_forall`

(root)

Definitions

Name	Category	Theorems
`PEquiv` 📖	CompData	34 math math: `Equiv.toPEquiv_apply`, `PEquiv.mem_iff_mem`, `PEquiv.single_apply_of_ne`, `PEquiv.trans_symm_eq_iff_forall_isSome`, `PEquiv.toMatrix_bot`, `PEquiv.mul_toMatrix_apply`, `PEquiv.trans_eq_some`, `PEquiv.ofSet_eq_some_iff`, `PEquiv.trans_eq_none`, `PEquiv.coe_mk`, `PEquiv.symm_trans_self`, `PEquiv.coe_mk_apply`, `PEquiv.refl_apply`, `PEquiv.ofSet_eq_some_self_iff`, `PEquiv.single_trans_single_of_ne`, `PEquiv.ext_iff`, `PEquiv.mem_trans`, `PEquiv.symm_bijective`, `PEquiv.mem_ofSet_self_iff`, `PEquiv.eq_some_iff`, `PEquiv.single_apply`, `PEquiv.mem_single`, `PEquiv.mem_ofSet_iff`, `PEquiv.toMatrix_injective`, `PEquiv.toMatrix_apply`, `PEquiv.toMatrix_mul_apply`, `PEquiv.symm_injective`, `PEquiv.symm_bot`, `PEquiv.le_def`, `PEquiv.bot_trans`, `PEquiv.self_trans_symm`, `PEquiv.mem_single_iff`, `PEquiv.trans_bot`, `PEquiv.bot_apply`
`«term_≃._»` 📖	CompOp	—

---

← Back to Index