MulOpposite

📁 Source: Mathlib/Algebra/Group/Subsemigroup/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_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_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_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_top`	80
Total	88

AddSubsemigroup

Definitions

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

Theorems

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

Subsemigroup

Definitions

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

Theorems

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

---

← Back to Index