Documentation Verification Report

Closure

📁 Source: Mathlib/GroupTheory/GroupAction/SubMulAction/Closure.lean

Statistics

Metric	Count
Definitions `closure`, `closure`	2
Theorems `closure_le`, `closure_mono`, `fg_iff`, `mem_closure`, `mem_closure_of_mem`, `subset_closure`, `closure_le`, `closure_mono`, `fg_iff`, `mem_closure`, `mem_closure_of_mem`, `subset_closure`	12
Total	14

SubAddAction

Definitions

Name	Category	Theorems
`closure` 📖	CompOp	6 math math: `closure_mono`, `subset_closure`, `mem_closure`, `mem_closure_of_mem`, `closure_le`, `fg_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_le` 📖	mathematical	—	`SubAddAction` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `mem_closure`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`SubAddAction` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	`closure_le` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure`
`fg_iff` 📖	mathematical	—	`FG` `closure` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Set.exists_finite_iff_finset`
`mem_closure` 📖	mathematical	—	`SubAddAction` `SetLike.instMembership` `instSetLike` `closure`	—	`Set.mem_iInter₂`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`SubAddAction` `SetLike.instMembership` `instSetLike` `closure`	—	`subset_closure`
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `SubAddAction` `instSetLike` `closure`	—	`mem_closure`

SubMulAction

Definitions

Name	Category	Theorems
`closure` 📖	CompOp	6 math math: `closure_le`, `mem_closure_of_mem`, `mem_closure`, `fg_iff`, `subset_closure`, `closure_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_le` 📖	mathematical	—	`SubMulAction` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `mem_closure`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`SubMulAction` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	`closure_le` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure`
`fg_iff` 📖	mathematical	—	`FG` `closure` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Set.exists_finite_iff_finset`
`mem_closure` 📖	mathematical	—	`SubMulAction` `SetLike.instMembership` `instSetLike` `closure`	—	`Set.mem_iInter₂`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`SubMulAction` `SetLike.instMembership` `instSetLike` `closure`	—	`subset_closure`
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `SubMulAction` `instSetLike` `closure`	—	`mem_closure`

---

← Back to Index