MulOpposite

📁 Source: Mathlib/Algebra/Group/Submonoid/MulOpposite.lean

Statistics

Metric	Count
Definitions `equivOp`, `op`, `opEquiv`, `unop`, `equivOp`, `op`, `opEquiv`, `unop`	8
Theorems `coe_op`, `coe_unop`, `equivOp_apply_coe`, `equivOp_symm_apply_coe`, `le_op_iff`, `mem_op`, `mem_unop`, `opEquiv_apply`, `opEquiv_symm_apply`, `op_bot`, `op_closure`, `op_eq_bot`, `op_eq_top`, `op_iInf`, `op_iSup`, `op_inf`, `op_inj`, `op_injective`, `op_le_iff`, `op_le_op_iff`, `op_sInf`, `op_sSup`, `op_sup`, `op_toSubsemigroup`, `op_top`, `op_unop`, `unop_bot`, `unop_closure`, `unop_eq_bot`, `unop_eq_top`, `unop_iInf`, `unop_iSup`, `unop_inf`, `unop_inj`, `unop_injective`, `unop_le_unop_iff`, `unop_op`, `unop_sInf`, `unop_sSup`, `unop_sup`, `unop_toSubsemigroup`, `unop_top`, `coe_op`, `coe_unop`, `equivOp_apply_coe`, `equivOp_symm_apply_coe`, `le_op_iff`, `mem_op`, `mem_unop`, `opEquiv_apply`, `opEquiv_symm_apply`, `op_bot`, `op_closure`, `op_eq_bot`, `op_eq_top`, `op_iInf`, `op_iSup`, `op_inf`, `op_inj`, `op_injective`, `op_le_iff`, `op_le_op_iff`, `op_sInf`, `op_sSup`, `op_sup`, `op_toSubsemigroup`, `op_top`, `op_unop`, `unop_bot`, `unop_closure`, `unop_eq_bot`, `unop_eq_top`, `unop_iInf`, `unop_iSup`, `unop_inf`, `unop_inj`, `unop_injective`, `unop_le_unop_iff`, `unop_op`, `unop_sInf`, `unop_sSup`, `unop_sup`, `unop_toSubsemigroup`, `unop_top`	84
Total	92

AddSubmonoid

Definitions

Name	Category	Theorems
`equivOp` 📖	CompOp	2 math math: `equivOp_apply_coe`, `equivOp_symm_apply_coe`
`op` 📖	CompOp	27 math math: `op_sup`, `op_inj`, `unop_op`, `op_eq_top`, `equivOp_apply_coe`, `op_eq_bot`, `AddSubgroup.op_toAddSubmonoid`, `mem_op`, `unop_sInf`, `op_top`, `op_le_op_iff`, `unop_sSup`, `op_inf`, `op_sSup`, `op_iSup`, `op_sInf`, `op_le_iff`, `op_closure`, `op_injective`, `coe_op`, `op_iInf`, `op_unop`, `opEquiv_apply`, `op_toSubsemigroup`, `equivOp_symm_apply_coe`, `le_op_iff`, `op_bot`
`opEquiv` 📖	CompOp	2 math math: `opEquiv_symm_apply`, `opEquiv_apply`
`unop` 📖	CompOp	25 math math: `unop_le_unop_iff`, `unop_inf`, `unop_op`, `unop_eq_bot`, `unop_iInf`, `unop_bot`, `unop_top`, `unop_inj`, `unop_iSup`, `unop_sInf`, `unop_closure`, `unop_sSup`, `mem_unop`, `coe_unop`, `op_sSup`, `op_sInf`, `op_le_iff`, `unop_injective`, `unop_eq_top`, `AddSubgroup.unop_toAddSubmonoid`, `unop_toSubsemigroup`, `opEquiv_symm_apply`, `unop_sup`, `op_unop`, `le_op_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_op` 📖	mathematical	—	`SetLike.coe` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `instSetLike` `op` `Set.preimage` `AddOpposite.unop`	—	—
`coe_unop` 📖	mathematical	—	`SetLike.coe` `AddSubmonoid` `instSetLike` `unop` `Set.preimage` `AddOpposite` `AddOpposite.op` `AddOpposite.instAddZeroClass`	—	—
`equivOp_apply_coe` 📖	mathematical	—	`AddOpposite` `AddSubmonoid` `AddOpposite.instAddZeroClass` `SetLike.instMembership` `instSetLike` `op` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivOp` `AddOpposite.op`	—	—
`equivOp_symm_apply_coe` 📖	mathematical	—	`AddSubmonoid` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `Equiv` `AddOpposite` `AddOpposite.instAddZeroClass` `op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivOp` `AddOpposite.unop`	—	—
`le_op_iff` 📖	mathematical	—	`AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `AddOpposite.op_surjective`
`mem_op` 📖	mathematical	—	`AddOpposite` `AddSubmonoid` `AddOpposite.instAddZeroClass` `SetLike.instMembership` `instSetLike` `op` `AddOpposite.unop`	—	—
`mem_unop` 📖	mathematical	—	`AddSubmonoid` `SetLike.instMembership` `instSetLike` `unop` `AddOpposite` `AddOpposite.instAddZeroClass` `AddOpposite.op`	—	—
`opEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `opEquiv` `op`	—	—
`opEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `opEquiv` `unop`	—	—
`op_bot` 📖	mathematical	—	`op` `Bot.bot` `AddSubmonoid` `instBot` `AddOpposite` `AddOpposite.instAddZeroClass`	—	`OrderIso.map_bot`
`op_closure` 📖	mathematical	—	`op` `closure` `AddOpposite` `AddOpposite.instAddZeroClass` `Set.preimage` `AddOpposite.unop`	—	`op_sInf` `Function.Surjective.forall` `AddOpposite.unop_surjective`
`op_eq_bot` 📖	mathematical	—	`op` `Bot.bot` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `instBot`	—	`op_injective` `op_bot`
`op_eq_top` 📖	mathematical	—	`op` `Top.top` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `instTop`	—	`op_injective` `op_top`
`op_iInf` 📖	mathematical	—	`op` `iInf` `AddSubmonoid` `instInfSet` `AddOpposite` `AddOpposite.instAddZeroClass`	—	`OrderIso.map_iInf`
`op_iSup` 📖	mathematical	—	`op` `iSup` `AddSubmonoid` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `AddOpposite` `AddOpposite.instAddZeroClass`	—	`OrderIso.map_iSup`
`op_inf` 📖	mathematical	—	`op` `AddSubmonoid` `instMin` `AddOpposite` `AddOpposite.instAddZeroClass`	—	—
`op_inj` 📖	mathematical	—	`op`	—	`RelIso.eq_iff_eq`
`op_injective` 📖	mathematical	—	`AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `op`	—	`OrderIso.injective`
`op_le_iff` 📖	mathematical	—	`AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `AddOpposite.op_surjective`
`op_le_op_iff` 📖	mathematical	—	`AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op`	—	`Function.Surjective.forall` `AddOpposite.op_surjective`
`op_sInf` 📖	mathematical	—	`op` `InfSet.sInf` `AddSubmonoid` `instInfSet` `AddOpposite` `AddOpposite.instAddZeroClass` `Set.preimage` `unop`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`op_sSup` 📖	mathematical	—	`op` `SupSet.sSup` `AddSubmonoid` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `AddOpposite` `AddOpposite.instAddZeroClass` `Set.preimage` `unop`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`op_sup` 📖	mathematical	—	`op` `AddSubmonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `AddOpposite` `AddOpposite.instAddZeroClass`	—	`OrderIso.map_sup`
`op_toSubsemigroup` 📖	mathematical	—	`toAddSubsemigroup` `AddOpposite` `AddOpposite.instAddZeroClass` `op` `AddSubsemigroup.op` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—
`op_top` 📖	mathematical	—	`op` `Top.top` `AddSubmonoid` `instTop` `AddOpposite` `AddOpposite.instAddZeroClass`	—	—
`op_unop` 📖	mathematical	—	`op` `unop`	—	—
`unop_bot` 📖	mathematical	—	`unop` `Bot.bot` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `instBot`	—	`OrderIso.map_bot`
`unop_closure` 📖	mathematical	—	`unop` `closure` `AddOpposite` `AddOpposite.instAddZeroClass` `Set.preimage` `AddOpposite.op`	—	`op_unop` `op_closure` `Set.preimage_preimage`
`unop_eq_bot` 📖	mathematical	—	`unop` `Bot.bot` `AddSubmonoid` `instBot` `AddOpposite` `AddOpposite.instAddZeroClass`	—	`unop_injective` `unop_bot`
`unop_eq_top` 📖	mathematical	—	`unop` `Top.top` `AddSubmonoid` `instTop` `AddOpposite` `AddOpposite.instAddZeroClass`	—	`unop_injective` `unop_top`
`unop_iInf` 📖	mathematical	—	`unop` `iInf` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `instInfSet`	—	`OrderIso.map_iInf`
`unop_iSup` 📖	mathematical	—	`unop` `iSup` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`OrderIso.map_iSup`
`unop_inf` 📖	mathematical	—	`unop` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `instMin`	—	—
`unop_inj` 📖	mathematical	—	`unop`	—	`RelIso.eq_iff_eq`
`unop_injective` 📖	mathematical	—	`AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `unop`	—	`OrderIso.injective`
`unop_le_unop_iff` 📖	mathematical	—	`AddSubmonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `unop` `AddOpposite` `AddOpposite.instAddZeroClass`	—	`Function.Surjective.forall` `AddOpposite.unop_surjective`
`unop_op` 📖	mathematical	—	`unop` `op`	—	—
`unop_sInf` 📖	mathematical	—	`unop` `InfSet.sInf` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `instInfSet` `Set.preimage` `op`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`unop_sSup` 📖	mathematical	—	`unop` `SupSet.sSup` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.preimage` `op`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`unop_sup` 📖	mathematical	—	`unop` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`OrderIso.map_sup`
`unop_toSubsemigroup` 📖	mathematical	—	`toAddSubsemigroup` `unop` `AddSubsemigroup.unop` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddOpposite` `AddOpposite.instAddZeroClass`	—	—
`unop_top` 📖	mathematical	—	`unop` `Top.top` `AddSubmonoid` `AddOpposite` `AddOpposite.instAddZeroClass` `instTop`	—	—

Submonoid

Definitions

Name	Category	Theorems
`equivOp` 📖	CompOp	2 math math: `equivOp_symm_apply_coe`, `equivOp_apply_coe`
`op` 📖	CompOp	36 math math: `le_op_iff`, `equivOp_symm_apply_coe`, `op_iInf`, `Subring.addEquivOp_apply_coe`, `Subsemiring.addEquivOp_apply_coe`, `op_eq_bot`, `op_sSup`, `op_sInf`, `op_inj`, `Subsemiring.addEquivOp_symm_apply_coe`, `op_iSup`, `coe_op`, `op_le_iff`, `op_sup`, `op_le_op_iff`, `equivOp_apply_coe`, `op_inf`, `unop_sInf`, `Subring.ringEquivOpMop_symm_apply_coe`, `opEquiv_apply`, `op_unop`, `Subsemiring.ringEquivOpMop_symm_apply_coe`, `unop_sSup`, `op_eq_top`, `op_closure`, `Subsemiring.op_toSubmonoid`, `op_injective`, `mem_op`, `Subgroup.op_toSubmonoid`, `Subalgebra.linearEquivOp_symm_apply_coe`, `Subalgebra.algEquivOpMop_symm_apply_coe`, `op_top`, `op_bot`, `unop_op`, `Subring.addEquivOp_symm_apply_coe`, `op_toSubsemigroup`
`opEquiv` 📖	CompOp	2 math math: `opEquiv_apply`, `opEquiv_symm_apply`
`unop` 📖	CompOp	26 math math: `le_op_iff`, `unop_eq_top`, `unop_iInf`, `unop_iSup`, `unop_inf`, `unop_inj`, `op_sSup`, `op_sInf`, `unop_top`, `op_le_iff`, `unop_eq_bot`, `unop_le_unop_iff`, `unop_sup`, `unop_sInf`, `op_unop`, `unop_sSup`, `unop_bot`, `unop_injective`, `mem_unop`, `unop_closure`, `coe_unop`, `Subsemiring.unop_toSubmonoid`, `opEquiv_symm_apply`, `Subgroup.unop_toSubmonoid`, `unop_op`, `unop_toSubsemigroup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_op` 📖	mathematical	—	`SetLike.coe` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `instSetLike` `op` `Set.preimage` `MulOpposite.unop`	—	—
`coe_unop` 📖	mathematical	—	`SetLike.coe` `Submonoid` `instSetLike` `unop` `Set.preimage` `MulOpposite` `MulOpposite.op` `MulOpposite.instMulOneClass`	—	—
`equivOp_apply_coe` 📖	mathematical	—	`MulOpposite` `Submonoid` `MulOpposite.instMulOneClass` `SetLike.instMembership` `instSetLike` `op` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivOp` `MulOpposite.op`	—	—
`equivOp_symm_apply_coe` 📖	mathematical	—	`Submonoid` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `Equiv` `MulOpposite` `MulOpposite.instMulOneClass` `op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivOp` `MulOpposite.unop`	—	—
`le_op_iff` 📖	mathematical	—	`Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`mem_op` 📖	mathematical	—	`MulOpposite` `Submonoid` `MulOpposite.instMulOneClass` `SetLike.instMembership` `instSetLike` `op` `MulOpposite.unop`	—	—
`mem_unop` 📖	mathematical	—	`Submonoid` `SetLike.instMembership` `instSetLike` `unop` `MulOpposite` `MulOpposite.instMulOneClass` `MulOpposite.op`	—	—
`opEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `opEquiv` `op`	—	—
`opEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `opEquiv` `unop`	—	—
`op_bot` 📖	mathematical	—	`op` `Bot.bot` `Submonoid` `instBot` `MulOpposite` `MulOpposite.instMulOneClass`	—	`OrderIso.map_bot`
`op_closure` 📖	mathematical	—	`op` `closure` `MulOpposite` `MulOpposite.instMulOneClass` `Set.preimage` `MulOpposite.unop`	—	`op_sInf` `Function.Surjective.forall` `MulOpposite.unop_surjective`
`op_eq_bot` 📖	mathematical	—	`op` `Bot.bot` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `instBot`	—	`op_injective` `op_bot`
`op_eq_top` 📖	mathematical	—	`op` `Top.top` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `instTop`	—	`op_injective` `op_top`
`op_iInf` 📖	mathematical	—	`op` `iInf` `Submonoid` `instInfSet` `MulOpposite` `MulOpposite.instMulOneClass`	—	`OrderIso.map_iInf`
`op_iSup` 📖	mathematical	—	`op` `iSup` `Submonoid` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `MulOpposite` `MulOpposite.instMulOneClass`	—	`OrderIso.map_iSup`
`op_inf` 📖	mathematical	—	`op` `Submonoid` `instMin` `MulOpposite` `MulOpposite.instMulOneClass`	—	—
`op_inj` 📖	mathematical	—	`op`	—	`RelIso.eq_iff_eq`
`op_injective` 📖	mathematical	—	`Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `op`	—	`OrderIso.injective`
`op_le_iff` 📖	mathematical	—	`Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`op_le_op_iff` 📖	mathematical	—	`Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`op_sInf` 📖	mathematical	—	`op` `InfSet.sInf` `Submonoid` `instInfSet` `MulOpposite` `MulOpposite.instMulOneClass` `Set.preimage` `unop`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`op_sSup` 📖	mathematical	—	`op` `SupSet.sSup` `Submonoid` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `MulOpposite` `MulOpposite.instMulOneClass` `Set.preimage` `unop`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`op_sup` 📖	mathematical	—	`op` `Submonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `MulOpposite` `MulOpposite.instMulOneClass`	—	`OrderIso.map_sup`
`op_toSubsemigroup` 📖	mathematical	—	`toSubsemigroup` `MulOpposite` `MulOpposite.instMulOneClass` `op` `Subsemigroup.op` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`op_top` 📖	mathematical	—	`op` `Top.top` `Submonoid` `instTop` `MulOpposite` `MulOpposite.instMulOneClass`	—	—
`op_unop` 📖	mathematical	—	`op` `unop`	—	—
`unop_bot` 📖	mathematical	—	`unop` `Bot.bot` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `instBot`	—	`OrderIso.map_bot`
`unop_closure` 📖	mathematical	—	`unop` `closure` `MulOpposite` `MulOpposite.instMulOneClass` `Set.preimage` `MulOpposite.op`	—	`op_unop` `op_closure` `Set.preimage_preimage`
`unop_eq_bot` 📖	mathematical	—	`unop` `Bot.bot` `Submonoid` `instBot` `MulOpposite` `MulOpposite.instMulOneClass`	—	`unop_injective` `unop_bot`
`unop_eq_top` 📖	mathematical	—	`unop` `Top.top` `Submonoid` `instTop` `MulOpposite` `MulOpposite.instMulOneClass`	—	`unop_injective` `unop_top`
`unop_iInf` 📖	mathematical	—	`unop` `iInf` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `instInfSet`	—	`OrderIso.map_iInf`
`unop_iSup` 📖	mathematical	—	`unop` `iSup` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`OrderIso.map_iSup`
`unop_inf` 📖	mathematical	—	`unop` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `instMin`	—	—
`unop_inj` 📖	mathematical	—	`unop`	—	`RelIso.eq_iff_eq`
`unop_injective` 📖	mathematical	—	`Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `unop`	—	`OrderIso.injective`
`unop_le_unop_iff` 📖	mathematical	—	`Submonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `unop` `MulOpposite` `MulOpposite.instMulOneClass`	—	`Function.Surjective.forall` `MulOpposite.unop_surjective`
`unop_op` 📖	mathematical	—	`unop` `op`	—	—
`unop_sInf` 📖	mathematical	—	`unop` `InfSet.sInf` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `instInfSet` `Set.preimage` `op`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`unop_sSup` 📖	mathematical	—	`unop` `SupSet.sSup` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.preimage` `op`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`unop_sup` 📖	mathematical	—	`unop` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`OrderIso.map_sup`
`unop_toSubsemigroup` 📖	mathematical	—	`toSubsemigroup` `unop` `Subsemigroup.unop` `MulOne.toMul` `MulOneClass.toMulOne` `MulOpposite` `MulOpposite.instMulOneClass`	—	—
`unop_top` 📖	mathematical	—	`unop` `Top.top` `Submonoid` `MulOpposite` `MulOpposite.instMulOneClass` `instTop`	—	—

---

← Back to Index