Theorems · Theorem · functional analysis

ConvexOn.sSup_of_countable_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 φ →
        ∃ 𝓕',
          𝓕'.Countable ∧
            sSup 𝓕' = s.domRestrict φ ∧
              ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑RCLike.re ∘ ⇑l) + Function.const (↑s) c

The countable version of sSup_affine_eq.

Defined in

Mathlib.Analysis.Convex.Approximation

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeTopologicalSpaceAddCommGroupModuleModuleIsScalarTowerIsTopologicalAddGroupContinuousSMulLocallyConvexSpaceHereditarilyLindelofSpace