Documentation Verification Report

AmpleSet

📁 Source: Mathlib/Analysis/Convex/AmpleSet.lean

Statistics

Metric	Count
Definitions `AmpleSet`	1
Theorems `image`, `image_iff`, `of_one_lt_codim`, `preimage`, `preimage_iff`, `union`, `vadd`, `vadd_iff`, `ampleSet_empty`, `ampleSet_univ`	10
Total	11

AmpleSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image` 📖	mathematical	`AmpleSet`	`Set.image` `DFunLike.coe` `ContinuousAffineEquiv` `Real` `Real.instRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineEquiv.instFunLike`	—	`Set.forall_mem_image` `Homeomorph.image_connectedComponentIn` `AffineMap.image_convexHull` `Set.image_univ` `Function.Surjective.range_eq` `ContinuousAffineEquiv.surjective`
`image_iff` 📖	mathematical	—	`AmpleSet` `Set.image` `DFunLike.coe` `ContinuousAffineEquiv` `Real` `Real.instRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineEquiv.instFunLike`	—	`image` `ContinuousAffineEquiv.symm_image_image`
`of_one_lt_codim` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.instOne` `Module.rank` `Real` `HasQuotient.Quotient` `Submodule` `Real.semiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Real.instRing` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	`AmpleSet` `Compl.compl` `Set` `Set.instCompl` `SetLike.coe` `Submodule.setLike`	—	`Submodule.connectedComponentIn_eq_self_of_one_lt_codim` `Set.eq_univ_iff_forall` `Submodule.eq_top_iff'` `rank_subsingleton'` `Real.instNontrivial` `Unique.instSubsingleton` `Cardinal.canonicallyOrderedAdd` `segment_subset_convexHull` `sub_eq_add_neg` `Submodule.add_mem_iff_right` `AddSubgroupClass.toNegMemClass` `Submodule.addSubgroupClass` `mem_segment_sub_add` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toCharZero` `subset_convexHull`
`preimage` 📖	mathematical	`AmpleSet`	`Set.preimage` `DFunLike.coe` `ContinuousAffineEquiv` `Real` `Real.instRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineEquiv.instFunLike`	—	`ContinuousAffineEquiv.image_symm_eq_preimage` `image`
`preimage_iff` 📖	mathematical	—	`AmpleSet` `Set.preimage` `DFunLike.coe` `ContinuousAffineEquiv` `Real` `Real.instRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `ContinuousAffineEquiv.instFunLike`	—	`image` `ContinuousAffineEquiv.image_preimage` `preimage`
`union` 📖	mathematical	`AmpleSet`	`Set` `Set.instUnion`	—	`Set.univ_subset_iff` `convexHull_mono` `connectedComponentIn_mono` `Set.subset_union_left` `Set.subset_union_right`
`vadd` 📖	mathematical	`AmpleSet`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `addGroupIsAddTorsor`	—	`image` `VAddCommClass.continuousConstVAdd` `vaddCommClass_self`
`vadd_iff` 📖	mathematical	—	`AmpleSet` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `addGroupIsAddTorsor`	—	`image_iff` `VAddCommClass.continuousConstVAdd` `vaddCommClass_self`

(root)

Definitions

Name	Category	Theorems
`AmpleSet` 📖	MathDef	6 math math: `AmpleSet.preimage_iff`, `AmpleSet.vadd_iff`, `AmpleSet.image_iff`, `AmpleSet.of_one_lt_codim`, `ampleSet_empty`, `ampleSet_univ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ampleSet_empty` 📖	mathematical	—	`AmpleSet` `Set` `Set.instEmptyCollection`	—	—
`ampleSet_univ` 📖	mathematical	—	`AmpleSet` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.univ`	—	`connectedComponentIn_univ` `PreconnectedSpace.connectedComponent_eq_univ` `ConnectedSpace.toPreconnectedSpace` `PathConnectedSpace.connectedSpace` `ContractibleSpace.instPathConnectedSpace` `RealTopologicalVectorSpace.contractibleSpace` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `convexHull_univ`

---

← Back to Index