Theorems · Theorem · functional analysis

RieszExtension.exists_top

∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s : PointedCone ℝ E) (p : E →ₗ.[ℝ] ℝ),
  (∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x) →
    (∀ (y : E), ∃ x, ↑x + y ∈ s) → ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), ↑x ∈ s → 0 ≤ ↑q x

Defined in

Mathlib.Analysis.Convex.Cone.Extension

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupModule