Documentation Verification Report

Approximation

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

Statistics

Metric	Count
Definitions	0
Theorems `convex_re_epigraph`, `exists_affine_le_of_lt`, `real_sSup_affine_eq`, `real_sSup_of_countable_affine_eq`, `real_sSup_of_nat_affine_eq`, `real_univ_sSup_affine_eq`, `real_univ_sSup_of_countable_affine_eq`, `real_univ_sSup_of_nat_affine_eq`, `sSup_affine_eq`, `sSup_of_countable_affine_eq`, `sSup_of_nat_affine_eq`, `univ_sSup_affine_eq`, `univ_sSup_of_countable_affine_eq`, `univ_sSup_of_nat_affine_eq`, `isClosed_re_epigraph`	15
Total	15

ConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convex_re_epigraph` 📖	mathematical	`ConvexOn` `Real` `Real.semiring` `Real.partialOrder` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`Convex` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Prod.instSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `setOf` `Set` `Set.instMembership` `Real.instLE` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `CommRing.toRing` `Field.toCommRing` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re`	—	`Convex.linear_preimage` `convex_epigraph` `Real.instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing`
`exists_affine_le_of_lt` 📖	mathematical	`Set` `Set.instMembership` `Real` `Real.instLT` `LowerSemicontinuousOn` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`Pi.hasLe` `Set.Elem` `Real.instLE` `Pi.instAdd` `Real.instAdd` `Set.restrict` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike`	—	`RCLike.geometric_hahn_banach_point_closed` `Prod.isScalarTower` `IsScalarTower.right` `Prod.instIsTopologicalAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Prod.continuousSMul` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Prod.locallyConvexSpace` `NormedSpace.toLocallyConvexSpace` `convex_re_epigraph` `LowerSemicontinuousOn.isClosed_re_epigraph` `RCLike.ofReal_re` `RingHomCompTriple.ids` `IsScalarTower.to_smulCommClass'` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smul_eq_mul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `smul_zero` `mul_one` `LT.lt.trans` `IsTopologicalSemiring.toContinuousAdd` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `RCLike.mul_re` `mul_comm` `RCLike.ofReal_im` `MulZeroClass.zero_mul` `sub_zero` `ContinuousLinearMap.coprod_comp_inl_inr` `IsTopologicalAddGroup.toContinuousAdd` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pos_of_right_mul_lt_le` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `lt_of_add_lt_add_left` `LT.lt.le` `neg_smul` `map_neg` `RCLike.smul_re` `mul_add` `Distrib.leftDistribClass` `inv_mul_cancel₀` `ne_of_gt` `one_mul` `mul_le_mul_of_nonneg_left` `neg_add_cancel_left`
`real_sSup_affine_eq` 📖	mathematical	`LowerSemicontinuousOn` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`SupSet.sSup` `Pi.supSet` `Set.Elem` `Real.instSupSet` `setOf` `Pi.hasLe` `Real.instLE` `Set.restrict` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `Pi.instAdd` `Real.instAdd` `DFunLike.coe` `ContinuousLinearMap.funLike`	—	`sSup_affine_eq` `IsScalarTower.left`
`real_sSup_of_countable_affine_eq` 📖	mathematical	`LowerSemicontinuousOn` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`Set.Countable` `SupSet.sSup` `Pi.supSet` `Set.Elem` `Real.instSupSet` `Set.restrict` `Pi.instAdd` `Real.instAdd` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike`	—	`sSup_of_countable_affine_eq` `IsScalarTower.left`
`real_sSup_of_nat_affine_eq` 📖	mathematical	`LowerSemicontinuousOn` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`iSup` `Pi.supSet` `Set.Elem` `Real.instSupSet` `Pi.instAdd` `Real.instAdd` `Set.restrict` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike`	—	`sSup_of_nat_affine_eq` `IsScalarTower.left`
`real_univ_sSup_affine_eq` 📖	mathematical	`LowerSemicontinuous` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.univ`	`SupSet.sSup` `Pi.supSet` `Real.instSupSet` `setOf` `Pi.hasLe` `Real.instLE` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `Pi.instAdd` `Real.instAdd` `DFunLike.coe` `ContinuousLinearMap.funLike`	—	`univ_sSup_affine_eq` `IsScalarTower.left`
`real_univ_sSup_of_countable_affine_eq` 📖	mathematical	`LowerSemicontinuous` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.univ`	`Set.Countable` `SupSet.sSup` `Pi.supSet` `Real.instSupSet` `Pi.instAdd` `Real.instAdd` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike`	—	`univ_sSup_of_countable_affine_eq` `IsScalarTower.left`
`real_univ_sSup_of_nat_affine_eq` 📖	mathematical	`LowerSemicontinuous` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.univ`	`iSup` `Pi.supSet` `Real.instSupSet` `Pi.instAdd` `Real.instAdd` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike`	—	`univ_sSup_of_nat_affine_eq` `IsScalarTower.left`
`sSup_affine_eq` 📖	mathematical	`LowerSemicontinuousOn` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`SupSet.sSup` `Pi.supSet` `Set.Elem` `Real.instSupSet` `setOf` `Pi.hasLe` `Real.instLE` `Set.restrict` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Pi.instAdd` `Real.instAdd` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `ContinuousLinearMap.funLike`	—	`sSup_apply` `csSup_eq_of_forall_le_of_forall_lt_exists_gt` `exists_affine_le_of_lt` `exists_between` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`
`sSup_of_countable_affine_eq` 📖	mathematical	`LowerSemicontinuousOn` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`Set.Countable` `SupSet.sSup` `Pi.supSet` `Set.Elem` `Real.instSupSet` `Set.restrict` `Pi.instAdd` `Real.instAdd` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike`	—	`isLUB_csSup` `exists_affine_le_of_lt` `Set.Nonempty.some_mem` `bddAbove_def` `sSup_affine_eq` `Continuous.lowerSemicontinuous` `instOrderTopologyReal` `Continuous.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Pi.continuous_restrict_apply` `Continuous.comp'` `RCLike.continuous_re` `ContinuousLinearMap.continuous` `continuous_const` `exists_countable_lowerSemicontinuous_isLUB` `instHereditarilyLindelofSpaceSubtype` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `IsLUB.csSup_eq` `instIsEmptyFalse`
`sSup_of_nat_affine_eq` 📖	mathematical	`LowerSemicontinuousOn` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`iSup` `Pi.supSet` `Set.Elem` `Real.instSupSet` `Pi.instAdd` `Real.instAdd` `Set.restrict` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike`	—	`sSup_of_countable_affine_eq` `Set.Countable.exists_eq_range` `sSup_range` `add_zero` `iSup_apply` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `ciSup_const` `Function.ne_iff` `Real.iSup_of_isEmpty` `Set.instIsEmptyElemEmptyCollection`
`univ_sSup_affine_eq` 📖	mathematical	`LowerSemicontinuous` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.univ`	`SupSet.sSup` `Pi.supSet` `Real.instSupSet` `setOf` `Pi.hasLe` `Real.instLE` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Pi.instAdd` `Real.instAdd` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `ContinuousLinearMap.funLike`	—	`sSup_affine_eq` `isClosed_univ` `lowerSemicontinuousOn_univ_iff` `sSup_image'` `sSup_eq_iSup'` `iSup_apply`
`univ_sSup_of_countable_affine_eq` 📖	mathematical	`LowerSemicontinuous` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.univ`	`Set.Countable` `SupSet.sSup` `Pi.supSet` `Real.instSupSet` `Pi.instAdd` `Real.instAdd` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike`	—	`isLUB_csSup` `exists_affine_le_of_lt` `Set.mem_univ` `isClosed_univ` `lowerSemicontinuousOn_univ_iff` `bddAbove_def` `univ_sSup_affine_eq` `Continuous.lowerSemicontinuous` `instOrderTopologyReal` `Continuous.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.comp'` `RCLike.continuous_re` `ContinuousLinearMap.continuous` `continuous_const` `exists_countable_lowerSemicontinuous_isLUB` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `IsLUB.csSup_eq`
`univ_sSup_of_nat_affine_eq` 📖	mathematical	`LowerSemicontinuous` `Real` `Real.instPreorder` `ConvexOn` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.univ`	`iSup` `Pi.supSet` `Real.instSupSet` `Pi.instAdd` `Real.instAdd` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike`	—	`univ_sSup_of_countable_affine_eq` `Set.Countable.exists_eq_range` `sSup_range` `add_zero` `iSup_apply` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `ciSup_const` `Real.iSup_of_isEmpty` `Set.instIsEmptyElemEmptyCollection`

LowerSemicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_re_epigraph` 📖	mathematical	`LowerSemicontinuousOn` `Real` `Real.instPreorder`	`IsClosed` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `setOf` `Set` `Set.instMembership` `Real.instLE` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re`	—	`IsClosed.preimage` `Continuous.prodMap` `continuous_id` `Continuous.comp` `continuous_coe_real_ereal` `ContinuousLinearMap.cont` `lowerSemicontinuousOn_iff_isClosed_epigraph` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `EReal.instOrderTopology` `Continuous.comp_lowerSemicontinuousOn` `instOrderTopologyReal` `StrictMono.monotone` `EReal.coe_strictMono`

---

← Back to Index