Theorems · Theorem · functional analysis

ConvexOn.sSup_of_nat_affine_eq

∀ {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E],
  IsClosed s →
    LowerSemicontinuousOn φ s →
      ConvexOn ℝ s φ →
        ∃ l c,
          (∀ (i : ℕ), s.domRestrict (⇑RCLike.re ∘ ⇑(l i)) + Function.const (↑s) (c i) ≤ s.domRestrict φ) ∧
            ⨆ i, s.domRestrict (⇑RCLike.re ∘ ⇑(l i)) + Function.const (↑s) (c i) = s.domRestrict φ

The sequential version of sSup_of_countable_affine_eq.

Defined in

Mathlib.Analysis.Convex.Approximation

Cited by

2 results in Mathlib

Foundations

Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeTopologicalSpaceAddCommGroupModuleModuleIsScalarTowerIsTopologicalAddGroupContinuousSMulLocallyConvexSpaceHereditarilyLindelofSpace