Theorems · Theorem · general topology

Convexity.continuous_convexCombPair_of_isBounded

∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] {T : Type u_3}
  [inst_3 : TopologicalSpace T] (f : T → ℝ),
  Continuous f →
    ∀ (hf0 : ∀ (t : T), 0 ≤ f t) (hf1 : ∀ (t : T), f t ≤ 1) (x y : T → X),
      ContinuousOn x (f ⁻¹' {0}ᶜ) →
        ContinuousOn y (f ⁻¹' {1}ᶜ) →
          Bornology.IsBounded (Set.range x) →
            Bornology.IsBounded (Set.range y) →
              Continuous fun i => Convexity.convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)

Defined in

Mathlib.Analysis.Convex.MetricSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

Convexity.ConvexSpaceMetricSpaceConvexity.IsConvexDistTopologicalSpace