Opposite

📁 Source: Mathlib/Data/Set/Opposite.lean

Statistics

Metric	Count
Definitions op, opEquiv, opEquiv_self, unop	4
Theorems mem_op, mem_unop, opEquiv_apply, opEquiv_self_apply_coe, opEquiv_self_symm_apply_coe, opEquiv_symm_apply, op_mem_op, op_unop, singleton_op, singleton_op_unop, singleton_unop, singleton_unop_op, unop_mem_unop, unop_op	14
Total	18

Set

Definitions

Name	Category	Theorems
op 📖	CompOp	9 math math: opEquiv_apply, opEquiv_self_symm_apply_coe, mem_op, op_unop, opEquiv_self_apply_coe, singleton_unop_op, unop_op, singleton_op, op_mem_op
opEquiv 📖	CompOp	2 math math: opEquiv_apply, opEquiv_symm_apply
opEquiv_self 📖	CompOp	2 math math: opEquiv_self_symm_apply_coe, opEquiv_self_apply_coe
unop 📖	CompOp	7 math math: mem_unop, op_unop, singleton_op_unop, unop_mem_unop, singleton_unop, unop_op, opEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_op 📖	mathematical	—	Opposite Set instMembership op Opposite.unop	—	—
mem_unop 📖	mathematical	—	Set instMembership unop Opposite Opposite.op	—	—
opEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Set Opposite EquivLike.toFunLike Equiv.instEquivLike opEquiv op	—	—
opEquiv_self_apply_coe 📖	mathematical	—	Set instMembership DFunLike.coe Equiv Elem Opposite op EquivLike.toFunLike Equiv.instEquivLike opEquiv_self Opposite.unop	—	—
opEquiv_self_symm_apply_coe 📖	mathematical	—	Opposite Set instMembership op DFunLike.coe Equiv Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm opEquiv_self Opposite.op	—	—
opEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Set Opposite EquivLike.toFunLike Equiv.instEquivLike Equiv.symm opEquiv unop	—	—
op_mem_op 📖	mathematical	—	Opposite Set instMembership op Opposite.op	—	—
op_unop 📖	mathematical	—	unop op	—	—
singleton_op 📖	mathematical	—	op Set instSingletonSet Opposite Opposite.op	—	ext Opposite.unop_injective Opposite.op_injective
singleton_op_unop 📖	mathematical	—	unop Opposite Set instSingletonSet Opposite.op	—	ext Opposite.op_injective Opposite.unop_injective
singleton_unop 📖	mathematical	—	unop Opposite Set instSingletonSet Opposite.unop	—	ext Opposite.op_injective Opposite.unop_injective
singleton_unop_op 📖	mathematical	—	op Set instSingletonSet Opposite.unop Opposite	—	ext Opposite.unop_injective Opposite.op_injective
unop_mem_unop 📖	mathematical	—	Set instMembership unop Opposite.unop Opposite	—	—
unop_op 📖	mathematical	—	op unop	—	—

---

← Back to Index