Documentation Verification Report

Extension

📁 Source: Mathlib/Analysis/Convex/Cone/Extension.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_top`, `step`, `exists_extension_of_le_sublinear`, `riesz_extension`	4
Total	4

RieszExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_top` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `LinearPMap.toFun'` `Real.instRing` `Real.instAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `ConvexCone` `Real.semiring` `Real.partialOrder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `ConvexCone.instSetLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`LinearPMap` `Real` `Real.instRing` `Real.instAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `LinearPMap.le` `LinearPMap.domain` `Top.top` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.instTop` `Real.instLE` `Real.instZero` `LinearPMap.toFun'`	—	`IsChain.directedOn` `instReflLe` `directedOn_image` `DirectedOn.mono` `StrictMono.monotone` `LinearPMap.domain_mono` `Submodule.mem_sSup_of_directed` `Set.Nonempty.image` `LinearPMap.le_sSup` `zorn_le_nonempty₀` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `step` `LT.lt.le` `LT.lt.ne'` `LE.le.antisymm`
`step` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `LinearPMap.toFun'` `Real.instRing` `Real.instAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `ConvexCone` `Real.semiring` `Real.partialOrder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `ConvexCone.instSetLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`LinearPMap` `Real` `Real.instRing` `Real.instAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `LinearPMap.semilatticeInf` `Real.instLE` `Real.instZero` `LinearPMap.toFun'`	—	`SetLike.exists_of_lt` `instIsConcreteLE` `lt_top_iff_ne_top` `exists_between_of_forall_le` `Set.Nonempty.image` `sub_eq_add_neg` `AddSubgroupClass.toNegMemClass` `Submodule.addSubgroupClass` `NegMemClass.coe_neg` `neg_neg` `ConvexCone.add_mem` `AddSubgroupClass.coe_sub` `add_sub_cancel` `add_assoc` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LinearPMap.map_sub` `lt_iff_le_not_ge` `LinearPMap.left_le_sup` `StrictMono.monotone` `LinearPMap.domain_mono` `Set.singleton_subset_iff` `Submodule.span_le` `sup_le_iff` `LinearPMap.domain_supSpanSingleton` `Submodule.mem_sup` `Submodule.mem_span_singleton` `smul_neg` `lt_trichotomy` `ConvexCone.smul_mem_iff` `Real.instIsStrictOrderedRing` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `smul_sub` `neg_smul` `smul_smul` `mul_inv_cancel₀` `LT.lt.ne` `one_smul` `IsScalarTower.left` `one_mul` `mul_assoc` `smul_eq_mul` `LinearPMap.map_smul` `neg_le_neg_iff` `neg_mul` `mul_le_mul_iff_right₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `zero_smul` `add_zero` `smul_add` `LT.lt.ne'`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_extension_of_le_sublinear` 📖	mathematical	`Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `Real.instMul` `Real.instLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Real.instAdd` `LinearPMap.toFun'` `Real.instRing` `Real.instAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain`	`LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `Semiring.toModule` `DFunLike.coe` `LinearMap.instFunLike` `Submodule` `Ring.toSemiring` `Real.instRing` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Real.instAddCommGroup` `LinearPMap.toFun'` `Real.instLE`	—	`mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `LT.lt.le` `LE.le.trans` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `add_zero` `le_trans` `Submodule.zero_mem` `zero_add` `sub_add_cancel` `riesz_extension` `sub_eq_neg_add` `RingHomCompTriple.ids` `zero_sub` `neg_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `neg_zero` `sub_self` `LinearPMap.map_zero` `sub_zero` `AddGroup.toOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `le_refl`
`riesz_extension` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `LinearPMap.toFun'` `Real.instRing` `Real.instAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `ConvexCone` `Real.semiring` `Real.partialOrder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `ConvexCone.instSetLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `Semiring.toModule` `DFunLike.coe` `LinearMap.instFunLike` `Submodule` `Ring.toSemiring` `Real.instRing` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Real.instAddCommGroup` `LinearPMap.toFun'` `Real.instLE` `Real.instZero`	—	`RieszExtension.exists_top` `RingHomCompTriple.ids`

---

← Back to Index