FunctionTopology

Statistics

Metric	Count
Definitions	0
Theorems `isClosed_setOf_concaveOn`, `isClosed_setOf_convexOn`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_setOf_concaveOn` 📖	mathematical	—	`IsClosed` `Pi.topologicalSpace` `setOf` `ConcaveOn`	—	`isClosed_setOf_convexOn` `instOrderClosedTopologyOrderDual` `instContinuousConstSMulOrderDual` `instContinuousAddOrderDual`
`isClosed_setOf_convexOn` 📖	mathematical	—	`IsClosed` `Pi.topologicalSpace` `setOf` `ConvexOn`	—	`Set.setOf_forall` `Set.iInter_congr_Prop` `IsClosed.inter` `isClosed_const` `isClosed_iInter` `isClosed_le` `continuous_apply` `Continuous.fun_add` `Continuous.const_smul`

---