Documentation Verification Report

Membership

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

Statistics

Metric	Count
Definitions	0
Theorems `add_mem_sup`, `coe_iSup_of_directed`, `coe_sSup_of_directed_on`, `iSup_induction`, `iSup_induction'`, `mem_biSup_of_directedOn`, `mem_iSup_of_directed`, `mem_iSup_of_mem`, `mem_iSup_prop`, `mem_sSup_of_directed_on`, `mem_sSup_of_mem`, `mem_sup_left`, `mem_sup_right`, `coe_iSup_of_directed`, `coe_sSup_of_directed_on`, `iSup_induction`, `iSup_induction'`, `mem_biSup_of_directedOn`, `mem_iSup_of_directed`, `mem_iSup_of_mem`, `mem_iSup_prop`, `mem_sSup_of_directed_on`, `mem_sSup_of_mem`, `mem_sup_left`, `mem_sup_right`, `mul_mem_sup`	26
Total	26

AddSubsemigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mem_sup` 📖	mathematical	`AddSubsemigroup` `SetLike.instMembership` `instSetLike`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`AddMemClass.add_mem` `instAddMemClass` `mem_sup_left` `mem_sup_right`
`coe_iSup_of_directed` 📖	mathematical	`Directed` `AddSubsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.iUnion`	—	`Set.ext` `SetLike.mem_coe` `mem_iSup_of_directed` `Set.mem_iUnion`
`coe_sSup_of_directed_on` 📖	mathematical	`DirectedOn` `AddSubsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `instSetLike` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.ext` `SetLike.mem_coe` `mem_sSup_of_directed_on` `Set.mem_iUnion`
`iSup_induction` 📖	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	—	`closure_induction` `Set.mem_iUnion` `iSup_eq_closure`
`iSup_induction'` 📖	—	`mem_iSup_of_mem` `AddMemClass.add_mem` `AddSubsemigroup` `instSetLike` `instAddMemClass` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `SetLike.instMembership`	—	—	`mem_iSup_of_mem` `AddMemClass.add_mem` `instAddMemClass` `iSup_induction`
`mem_biSup_of_directedOn` 📖	mathematical	`DirectedOn` `Function.onFun` `AddSubsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `setOf`	`SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`closure_induction` `Set.mem_iUnion` `SetLike.mem_coe` `AddMemClass.add_mem` `instAddMemClass` `closure_iUnion` `iSup_congr_Prop` `closure_eq` `le_iSup` `iSup_pos`
`mem_iSup_of_directed` 📖	mathematical	`Directed` `AddSubsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`iSup_pos` `iSup_plift_down` `mem_biSup_of_directedOn` `directedOn_onFun_iff` `Set.image_univ` `directedOn_range` `PLift.exists`
`mem_iSup_of_mem` 📖	mathematical	`AddSubsemigroup` `SetLike.instMembership` `instSetLike`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`le_iSup`
`mem_iSup_prop` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`iSup_congr_Prop` `iSup_pos` `iSup_neg` `IsEmpty.exists_iff` `instIsEmptyFalse`
`mem_sSup_of_directed_on` 📖	mathematical	`DirectedOn` `AddSubsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set` `Set.instMembership`	—	`sSup_eq_iSup'` `mem_iSup_of_directed` `DirectedOn.directed_val` `SetCoe.exists`
`mem_sSup_of_mem` 📖	mathematical	`AddSubsemigroup` `Set` `Set.instMembership` `SetLike.instMembership` `instSetLike`	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`le_sSup`
`mem_sup_left` 📖	mathematical	`AddSubsemigroup` `SetLike.instMembership` `instSetLike`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`le_sup_left`
`mem_sup_right` 📖	mathematical	`AddSubsemigroup` `SetLike.instMembership` `instSetLike`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`le_sup_right`

Subsemigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_iSup_of_directed` 📖	mathematical	`Directed` `Subsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.iUnion`	—	`Set.ext` `mem_iSup_of_directed`
`coe_sSup_of_directed_on` 📖	mathematical	`DirectedOn` `Subsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `instSetLike` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.ext` `mem_sSup_of_directed_on`
`iSup_induction` 📖	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	—	`closure_induction` `Set.mem_iUnion` `iSup_eq_closure`
`iSup_induction'` 📖	—	`mem_iSup_of_mem` `MulMemClass.mul_mem` `Subsemigroup` `instSetLike` `instMulMemClass` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `SetLike.instMembership`	—	—	`mem_iSup_of_mem` `MulMemClass.mul_mem` `instMulMemClass` `iSup_induction`
`mem_biSup_of_directedOn` 📖	mathematical	`DirectedOn` `Function.onFun` `Subsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `setOf`	`SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`closure_induction` `MulMemClass.mul_mem` `instMulMemClass` `closure_iUnion` `iSup_congr_Prop` `closure_eq` `le_iSup` `iSup_pos`
`mem_iSup_of_directed` 📖	mathematical	`Directed` `Subsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`iSup_pos` `iSup_plift_down` `mem_biSup_of_directedOn` `directedOn_onFun_iff` `Set.image_univ` `directedOn_range`
`mem_iSup_of_mem` 📖	mathematical	`Subsemigroup` `SetLike.instMembership` `instSetLike`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`le_iSup`
`mem_iSup_prop` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`iSup_congr_Prop` `iSup_pos` `iSup_neg` `instIsEmptyFalse`
`mem_sSup_of_directed_on` 📖	mathematical	`DirectedOn` `Subsemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set` `Set.instMembership`	—	`sSup_eq_iSup'` `mem_iSup_of_directed` `DirectedOn.directed_val`
`mem_sSup_of_mem` 📖	mathematical	`Subsemigroup` `Set` `Set.instMembership` `SetLike.instMembership` `instSetLike`	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`le_sSup`
`mem_sup_left` 📖	mathematical	`Subsemigroup` `SetLike.instMembership` `instSetLike`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`le_sup_left`
`mem_sup_right` 📖	mathematical	`Subsemigroup` `SetLike.instMembership` `instSetLike`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`le_sup_right`
`mul_mem_sup` 📖	mathematical	`Subsemigroup` `SetLike.instMembership` `instSetLike`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`MulMemClass.mul_mem` `instMulMemClass` `mem_sup_left` `mem_sup_right`

---

← Back to Index