Basic

📁 Source: Mathlib/Algebra/Group/Subsemigroup/Basic.lean

Statistics

Metric	Count
Definitions `ofDense`, `closure`, `gi`, `instCompleteLattice`, `instInfSet`, `ofDense`, `closure`, `gi`, `instCompleteLattice`, `instInfSet`	10
Theorems `coe_ofDense`, `eqOn_closure`, `eq_of_eqOn_dense`, `closure_empty`, `closure_eq`, `closure_eq_of_le`, `closure_iUnion`, `closure_induction`, `closure_induction₂`, `closure_le`, `closure_mono`, `closure_singleton_le_iff_mem`, `closure_union`, `closure_univ`, `coe_iInf`, `coe_sInf`, `dense_induction`, `iSup_eq_closure`, `mem_closure`, `mem_closure_of_mem`, `mem_iInf`, `mem_iSup`, `mem_sInf`, `notMem_of_notMem_closure`, `subset_closure`, `coe_ofDense`, `eqOn_closure`, `eq_of_eqOn_dense`, `closure_empty`, `closure_eq`, `closure_eq_of_le`, `closure_iUnion`, `closure_induction`, `closure_induction₂`, `closure_le`, `closure_mono`, `closure_singleton_le_iff_mem`, `closure_union`, `closure_univ`, `coe_iInf`, `coe_sInf`, `dense_induction`, `iSup_eq_closure`, `mem_closure`, `mem_closure_of_mem`, `mem_iInf`, `mem_iSup`, `mem_sInf`, `notMem_of_notMem_closure`, `subset_closure`	50
Total	60

AddHom

Definitions

Name	Category	Theorems
`ofDense` 📖	CompOp	1 math math: `coe_ofDense`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_ofDense` 📖	mathematical	`AddSubsemigroup.closure` `AddSemigroup.toAdd` `Top.top` `AddSubsemigroup` `AddSubsemigroup.instTop`	`DFunLike.coe` `AddHom` `funLike` `ofDense`	—	—
`eqOn_closure` 📖	mathematical	`Set.EqOn` `DFunLike.coe` `AddHom` `funLike`	`SetLike.coe` `AddSubsemigroup` `AddSubsemigroup.instSetLike` `AddSubsemigroup.closure`	—	`AddSubsemigroup.closure_le`
`eq_of_eqOn_dense` 📖	—	`AddSubsemigroup.closure` `Top.top` `AddSubsemigroup` `AddSubsemigroup.instTop` `Set.EqOn` `DFunLike.coe` `AddHom` `funLike`	—	—	`eq_of_eqOn_top` `eqOn_closure`

AddSubsemigroup

Definitions

Name	Category	Theorems
`closure` 📖	CompOp	23 math math: `closure_iUnion`, `closure_le_centralizer_centralizer`, `mem_closure`, `closure_univ`, `toSubsemigroup'_closure`, `mem_closure_of_mem`, `AddHom.eqOn_closure`, `subset_closure`, `Subsemigroup.toAddSubsemigroup_closure`, `closure_closure_coe_preimage`, `closure_eq`, `closure_singleton_le_iff_mem`, `iSup_eq_closure`, `closure_le`, `closure_union`, `op_closure`, `toSubsemigroup_closure`, `AddHom.mclosure_preimage_le`, `closure_mono`, `closure_empty`, `Subsemigroup.toAddSubsemigroup'_closure`, `unop_closure`, `AddHom.map_mclosure`
`gi` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	27 math math: `closure_iUnion`, `op_iSup`, `coe_iSup_of_directed`, `map_sup`, `unop_sSup`, `unop_iSup`, `map_iSup`, `mem_iSup`, `mem_biSup_of_directedOn`, `comap_sup_map_of_injective`, `mem_sup_left`, `unop_sup`, `mem_iSup_of_mem`, `op_sup`, `op_sSup`, `comap_iSup_map_of_injective`, `iSup_eq_closure`, `mem_sup_right`, `map_iSup_comap_of_surjective`, `mem_sSup_of_mem`, `map_sup_comap_of_surjective`, `mem_iSup_prop`, `mem_sSup_of_directed_on`, `coe_sSup_of_directed_on`, `closure_union`, `add_mem_sup`, `mem_iSup_of_directed`
`instInfSet` 📖	CompOp	12 math math: `unop_iInf`, `comap_iInf`, `op_iInf`, `op_sInf`, `mem_iInf`, `coe_sInf`, `unop_sInf`, `map_iInf_comap_of_surjective`, `mem_sInf`, `comap_iInf_map_of_injective`, `map_iInf`, `coe_iInf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_empty` 📖	mathematical	—	`closure` `Set` `Set.instEmptyCollection` `Bot.bot` `AddSubsemigroup` `instBot`	—	`GaloisConnection.l_bot` `GaloisInsertion.gc`
`closure_eq` 📖	mathematical	—	`closure` `SetLike.coe` `AddSubsemigroup` `instSetLike`	—	`GaloisInsertion.l_u_eq`
`closure_eq_of_le` 📖	—	`Set` `Set.instHasSubset` `SetLike.coe` `AddSubsemigroup` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	—	`le_antisymm` `closure_le`
`closure_iUnion` 📖	mathematical	—	`closure` `Set.iUnion` `iSup` `AddSubsemigroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `GaloisInsertion.gc`
`closure_induction` 📖	—	`subset_closure` `AddMemClass.add_mem` `AddSubsemigroup` `instSetLike` `instAddMemClass` `closure` `SetLike.instMembership`	—	—	`subset_closure` `AddMemClass.add_mem` `instAddMemClass` `closure_le`
`closure_induction₂` 📖	—	`subset_closure` `AddMemClass.add_mem` `AddSubsemigroup` `instSetLike` `instAddMemClass` `closure` `SetLike.instMembership`	—	—	`subset_closure` `AddMemClass.add_mem` `instAddMemClass` `closure_induction`
`closure_le` 📖	mathematical	—	`AddSubsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`Set.Subset.trans` `subset_closure` `sInf_le`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`AddSubsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	`closure_le` `Set.Subset.trans` `subset_closure`
`closure_singleton_le_iff_mem` 📖	mathematical	—	`AddSubsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instSingletonSet` `SetLike.instMembership` `instSetLike`	—	`closure_le` `Set.singleton_subset_iff` `SetLike.mem_coe`
`closure_union` 📖	mathematical	—	`closure` `Set` `Set.instUnion` `AddSubsemigroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `GaloisInsertion.gc`
`closure_univ` 📖	mathematical	—	`closure` `Set.univ` `Top.top` `AddSubsemigroup` `instTop`	—	`closure_eq` `coe_top`
`coe_iInf` 📖	mathematical	—	`SetLike.coe` `AddSubsemigroup` `instSetLike` `iInf` `instInfSet` `Set.iInter`	—	`Set.biInter_range`
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `AddSubsemigroup` `instSetLike` `InfSet.sInf` `instInfSet` `Set.iInter` `Set` `Set.instMembership`	—	—
`dense_induction` 📖	—	`closure` `Top.top` `AddSubsemigroup` `instTop`	—	—	`closure_induction` `mem_top`
`iSup_eq_closure` 📖	mathematical	—	`iSup` `AddSubsemigroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `closure` `Set.iUnion` `SetLike.coe` `instSetLike`	—	`closure_iUnion` `closure_eq`
`mem_closure` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `closure`	—	`mem_sInf`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `closure`	—	`subset_closure`
`mem_iInf` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet`	—	`mem_sInf` `Set.forall_mem_range`
`mem_iSup` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`closure_singleton_le_iff_mem` `le_iSup_iff`
`mem_sInf` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`Set.mem_iInter₂`
`notMem_of_notMem_closure` 📖	mathematical	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `closure`	`Set` `Set.instMembership`	—	`subset_closure`
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `AddSubsemigroup` `instSetLike` `closure`	—	`mem_closure`

MulHom

Definitions

Name	Category	Theorems
`ofDense` 📖	CompOp	1 math math: `coe_ofDense`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_ofDense` 📖	mathematical	`Subsemigroup.closure` `Semigroup.toMul` `Top.top` `Subsemigroup` `Subsemigroup.instTop`	`DFunLike.coe` `MulHom` `funLike` `ofDense`	—	—
`eqOn_closure` 📖	mathematical	`Set.EqOn` `DFunLike.coe` `MulHom` `funLike`	`SetLike.coe` `Subsemigroup` `Subsemigroup.instSetLike` `Subsemigroup.closure`	—	`Subsemigroup.closure_le`
`eq_of_eqOn_dense` 📖	—	`Subsemigroup.closure` `Top.top` `Subsemigroup` `Subsemigroup.instTop` `Set.EqOn` `DFunLike.coe` `MulHom` `funLike`	—	—	`eq_of_eqOn_top` `eqOn_closure`

Subsemigroup

Definitions

Name	Category	Theorems
`closure` 📖	CompOp	30 math math: `AddSubsemigroup.toSubsemigroup'_closure`, `MulHom.mclosure_preimage_le`, `closure_empty`, `Submonoid.closure_eq_one_union`, `closure_le_centralizer_centralizer`, `MulHom.eqOn_closure`, `NonUnitalStarAlgebra.adjoin_eq_span`, `toAddSubsemigroup_closure`, `closure_le`, `closure_union`, `NonUnitalSubsemiring.closure_subsemigroup_closure`, `MulHom.map_mclosure`, `mem_closure`, `closure_closure_coe_preimage`, `mem_closure_of_mem`, `closure_singleton_le_iff_mem`, `closure_iUnion`, `op_closure`, `subset_closure`, `closure_eq`, `NonUnitalSubring.mem_closure_iff`, `unop_closure`, `AddSubsemigroup.toSubsemigroup_closure`, `iSup_eq_closure`, `closure_mono`, `NonUnitalSubsemiring.mem_closure_iff`, `NonUnitalSubsemiring.coe_closure_eq`, `toAddSubsemigroup'_closure`, `closure_univ`, `NonUnitalAlgebra.adjoin_eq_span`
`gi` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	27 math math: `unop_iSup`, `mem_sSup_of_mem`, `mem_iSup_prop`, `mul_mem_sup`, `mem_iSup_of_directed`, `mem_sSup_of_directed_on`, `map_sup`, `mem_biSup_of_directedOn`, `closure_union`, `unop_sup`, `comap_sup_map_of_injective`, `comap_iSup_map_of_injective`, `mem_sup_left`, `op_sup`, `op_iSup`, `closure_iUnion`, `mem_iSup_of_mem`, `mem_iSup`, `mem_sup_right`, `map_iSup`, `map_iSup_comap_of_surjective`, `coe_iSup_of_directed`, `iSup_eq_closure`, `map_sup_comap_of_surjective`, `coe_sSup_of_directed_on`, `unop_sSup`, `op_sSup`
`instInfSet` 📖	CompOp	14 math math: `map_iInf_comap_of_surjective`, `op_iInf`, `coe_sInf`, `NonUnitalSubring.sInf_toSubsemigroup`, `comap_iInf_map_of_injective`, `mem_iInf`, `map_iInf`, `mem_sInf`, `op_sInf`, `unop_sInf`, `NonUnitalSubsemiring.sInf_toSubsemigroup`, `unop_iInf`, `coe_iInf`, `comap_iInf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_empty` 📖	mathematical	—	`closure` `Set` `Set.instEmptyCollection` `Bot.bot` `Subsemigroup` `instBot`	—	`GaloisConnection.l_bot` `GaloisInsertion.gc`
`closure_eq` 📖	mathematical	—	`closure` `SetLike.coe` `Subsemigroup` `instSetLike`	—	`GaloisInsertion.l_u_eq`
`closure_eq_of_le` 📖	—	`Set` `Set.instHasSubset` `SetLike.coe` `Subsemigroup` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	—	`le_antisymm` `closure_le`
`closure_iUnion` 📖	mathematical	—	`closure` `Set.iUnion` `iSup` `Subsemigroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `GaloisInsertion.gc`
`closure_induction` 📖	—	`subset_closure` `MulMemClass.mul_mem` `Subsemigroup` `instSetLike` `instMulMemClass` `closure` `SetLike.instMembership`	—	—	`subset_closure` `MulMemClass.mul_mem` `instMulMemClass` `closure_le`
`closure_induction₂` 📖	—	`subset_closure` `MulMemClass.mul_mem` `Subsemigroup` `instSetLike` `instMulMemClass` `closure` `SetLike.instMembership`	—	—	`subset_closure` `MulMemClass.mul_mem` `instMulMemClass` `closure_induction`
`closure_le` 📖	mathematical	—	`Subsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`Set.Subset.trans` `subset_closure` `sInf_le`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`Subsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	`closure_le` `Set.Subset.trans` `subset_closure`
`closure_singleton_le_iff_mem` 📖	mathematical	—	`Subsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instSingletonSet` `SetLike.instMembership` `instSetLike`	—	`closure_le` `Set.singleton_subset_iff` `SetLike.mem_coe`
`closure_union` 📖	mathematical	—	`closure` `Set` `Set.instUnion` `Subsemigroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `GaloisInsertion.gc`
`closure_univ` 📖	mathematical	—	`closure` `Set.univ` `Top.top` `Subsemigroup` `instTop`	—	`closure_eq` `coe_top`
`coe_iInf` 📖	mathematical	—	`SetLike.coe` `Subsemigroup` `instSetLike` `iInf` `instInfSet` `Set.iInter`	—	`Set.biInter_range`
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `Subsemigroup` `instSetLike` `InfSet.sInf` `instInfSet` `Set.iInter` `Set` `Set.instMembership`	—	—
`dense_induction` 📖	—	`closure` `Top.top` `Subsemigroup` `instTop`	—	—	`closure_induction` `mem_top`
`iSup_eq_closure` 📖	mathematical	—	`iSup` `Subsemigroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `closure` `Set.iUnion` `SetLike.coe` `instSetLike`	—	`closure_iUnion` `closure_eq`
`mem_closure` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `closure`	—	`mem_sInf`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`Subsemigroup` `SetLike.instMembership` `instSetLike` `closure`	—	`subset_closure`
`mem_iInf` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet`	—	—
`mem_iSup` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`closure_singleton_le_iff_mem` `le_iSup_iff`
`mem_sInf` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`Set.mem_iInter₂`
`notMem_of_notMem_closure` 📖	mathematical	`Subsemigroup` `SetLike.instMembership` `instSetLike` `closure`	`Set` `Set.instMembership`	—	`subset_closure`
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Subsemigroup` `instSetLike` `closure`	—	`mem_closure`

---

← Back to Index