ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>↑‖x‖₊ ≤ egauge 𝕜 (Metric.ball 0 1) x
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>x : E<VAR>r : ℝ≥0<VAR>hc : 1 < ‖c‖<VAR>h₀ : r ≠ 0 ∨ x ≠ 0<GOAL>egauge 𝕜 (Metric.ball 0 ↑r) x ≤ ↑‖c‖₊ * ↑‖x‖₊ / ↑r
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<GOAL>egauge 𝕜 (Metric.ball 0 1) x ≤ ↑‖c‖₊ * ↑‖x‖₊
<VAR>r : ℝ<GOAL>Convex ℝ {c | c.re < r}
<VAR>r : ℝ<GOAL>Convex ℝ {c | c.re ≤ r}
<VAR>r : ℝ<GOAL>Convex ℝ {c | r < c.re}
<VAR>r : ℝ<GOAL>Convex ℝ {c | r ≤ c.re}
<VAR>r : ℝ<GOAL>Convex ℝ {c | c.im < r}
<VAR>r : ℝ<GOAL>Convex ℝ {c | c.im ≤ r}
<VAR>r : ℝ<GOAL>Convex ℝ {c | r < c.im}
<VAR>r : ℝ<GOAL>Convex ℝ {c | r ≤ c.im}
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_mono : MonotoneOn (deriv f) (interior D)<GOAL>ConvexOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>h_anti : AntitoneOn (deriv f) (interior D)<GOAL>ConcaveOn ℝ D f
<VAR>x y : ℝ<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f (Set.Icc x y)<VAR>hxy : x < y<VAR>hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)<VAR>h : ∀ w ∈ Set.Ioo x y, deriv f w ≠ 0<GOAL>∃ a ∈ Set.Ioo x y, (f y - f x) / (y - x) < deriv f a
<VAR>x y : ℝ<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f (Set.Icc x y)<VAR>hxy : x < y<VAR>hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)<GOAL>∃ a ∈ Set.Ioo x y, (f y - f x) / (y - x) < deriv f a
<VAR>x y : ℝ<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f (Set.Icc x y)<VAR>hxy : x < y<VAR>hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)<VAR>h : ∀ w ∈ Set.Ioo x y, deriv f w ≠ 0<GOAL>∃ a ∈ Set.Ioo x y, deriv f a < (f y - f x) / (y - x)
<VAR>x y : ℝ<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f (Set.Icc x y)<VAR>hxy : x < y<VAR>hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)<GOAL>∃ a ∈ Set.Ioo x y, deriv f a < (f y - f x) / (y - x)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : StrictMonoOn (deriv f) (interior D)<GOAL>StrictConvexOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>h_anti : StrictAntiOn (deriv f) (interior D)<GOAL>StrictConcaveOn ℝ D f
<VAR>f : ℝ → ℝ<VAR>hf : Differentiable ℝ f<VAR>hf'_mono : Monotone (deriv f)<GOAL>ConvexOn ℝ Set.univ f
<VAR>f : ℝ → ℝ<VAR>hf : Differentiable ℝ f<VAR>hf'_anti : Antitone (deriv f)<GOAL>ConcaveOn ℝ Set.univ f
<VAR>f : ℝ → ℝ<VAR>hf : Continuous f<VAR>hf'_mono : StrictMono (deriv f)<GOAL>StrictConvexOn ℝ Set.univ f
<VAR>f : ℝ → ℝ<VAR>hf : Continuous f<VAR>hf'_anti : StrictAnti (deriv f)<GOAL>StrictConcaveOn ℝ Set.univ f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'' : DifferentiableOn ℝ (deriv f) (interior D)<VAR>hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x<GOAL>ConvexOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'' : DifferentiableOn ℝ (deriv f) (interior D)<VAR>hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0<GOAL>ConcaveOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf'' : ∀ x ∈ interior D, 0 < deriv^[2] f x<GOAL>StrictConvexOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf'' : ∀ x ∈ interior D, deriv^[2] f x < 0<GOAL>StrictConcaveOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf' : DifferentiableOn ℝ f D<VAR>hf'' : DifferentiableOn ℝ (deriv f) D<VAR>hf''_nonneg : ∀ x ∈ D, 0 ≤ deriv^[2] f x<GOAL>ConvexOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf' : DifferentiableOn ℝ f D<VAR>hf'' : DifferentiableOn ℝ (deriv f) D<VAR>hf''_nonpos : ∀ x ∈ D, deriv^[2] f x ≤ 0<GOAL>ConcaveOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf'' : ∀ x ∈ D, 0 < deriv^[2] f x<GOAL>StrictConvexOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf'' : ∀ x ∈ D, deriv^[2] f x < 0<GOAL>StrictConcaveOn ℝ D f
<VAR>f : ℝ → ℝ<VAR>hf' : Differentiable ℝ f<VAR>hf'' : Differentiable ℝ (deriv f)<VAR>hf''_nonneg : ∀ (x : ℝ), 0 ≤ deriv^[2] f x<GOAL>ConvexOn ℝ Set.univ f
<VAR>f : ℝ → ℝ<VAR>hf' : Differentiable ℝ f<VAR>hf'' : Differentiable ℝ (deriv f)<VAR>hf''_nonpos : ∀ (x : ℝ), deriv^[2] f x ≤ 0<GOAL>ConcaveOn ℝ Set.univ f
<VAR>f : ℝ → ℝ<VAR>hf : Continuous f<VAR>hf'' : ∀ (x : ℝ), 0 < deriv^[2] f x<GOAL>StrictConvexOn ℝ Set.univ f
<VAR>f : ℝ → ℝ<VAR>hf : Continuous f<VAR>hf'' : ∀ (x : ℝ), deriv^[2] f x < 0<GOAL>StrictConcaveOn ℝ Set.univ f
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>x : 𝕜<VAR>hfc : ConvexOn 𝕜 s f<VAR>hx : x ∈ s<GOAL>MonotoneOn (slope f x) (s \ {x})
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>x : 𝕜<VAR>hfc : ConcaveOn 𝕜 s f<VAR>hx : x ∈ s<GOAL>AntitoneOn (slope f x) (s \ {x})
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Set.Ioi x) x<GOAL>f' ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f (Set.Ioi x) x<GOAL>derivWithin f (Set.Ioi x) x ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f S x<GOAL>derivWithin f S x ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>ha : HasDerivAt f f' x<GOAL>f' ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableAt ℝ f x<GOAL>deriv f x ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Set.Iio y) y<GOAL>slope f x y ≤ f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f (Set.Iio y) y<GOAL>slope f x y ≤ derivWithin f (Set.Iio y) y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f S y<GOAL>slope f x y ≤ derivWithin f S y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivAt f f' y<GOAL>slope f x y ≤ f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableAt ℝ f y<GOAL>slope f x y ≤ deriv f y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<GOAL>MonotoneOn (derivWithin f S) S
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hfd : ∀ x ∈ S, DifferentiableAt ℝ f x<GOAL>MonotoneOn (deriv f) S
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Set.Ioi x) x<GOAL>f' < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f (Set.Ioi x) x<GOAL>derivWithin f (Set.Ioi x) x < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f S x<GOAL>derivWithin f S x < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivAt f f' x<GOAL>f' < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableAt ℝ f x<GOAL>deriv f x < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Set.Iio y) y<GOAL>slope f x y < f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f (Set.Iio y) y<GOAL>slope f x y < derivWithin f (Set.Iio y) y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f S y<GOAL>slope f x y < derivWithin f S y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivAt f f' y<GOAL>slope f x y < f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableAt ℝ f y<GOAL>slope f x y < deriv f y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<GOAL>StrictMonoOn (derivWithin f S) S
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hfd : ∀ x ∈ S, DifferentiableAt ℝ f x<GOAL>StrictMonoOn (deriv f) S
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Set.Ioi x) x<GOAL>slope f x y ≤ f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f (Set.Ioi x) x<GOAL>slope f x y ≤ derivWithin f (Set.Ioi x) x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f S x<GOAL>slope f x y ≤ derivWithin f S x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivAt f f' x<GOAL>slope f x y ≤ f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableAt ℝ f x<GOAL>slope f x y ≤ deriv f x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Set.Iio y) y<GOAL>f' ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f (Set.Iio y) y<GOAL>derivWithin f (Set.Iio y) y ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f S y<GOAL>derivWithin f S y ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivAt f f' y<GOAL>f' ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableAt ℝ f y<GOAL>deriv f y ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<GOAL>AntitoneOn (derivWithin f S) S
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hfd : ∀ x ∈ S, DifferentiableAt ℝ f x<GOAL>AntitoneOn (deriv f) S
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Set.Ioi x) x<GOAL>slope f x y < f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f (Set.Ioi x) x<GOAL>slope f x y < derivWithin f (Set.Ioi x) x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f S x<GOAL>slope f x y < derivWithin f S x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableAt ℝ f x<GOAL>slope f x y < deriv f x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Set.Iio y) y<GOAL>f' < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f (Set.Iio y) y<GOAL>derivWithin f (Set.Iio y) y < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableWithinAt ℝ f S y<GOAL>derivWithin f S y < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivAt f f' y<GOAL>f' < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : DifferentiableAt ℝ f y<GOAL>deriv f y < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<GOAL>StrictAntiOn (derivWithin f S) S
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hfd : ∀ x ∈ S, DifferentiableAt ℝ f x<GOAL>StrictAntiOn (deriv f) S
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : Convex 𝕜 s<VAR>hx : x ∈ s<GOAL>StarConvex 𝕜 x s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<GOAL>Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → [x-[𝕜]y] ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>h : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>[x-[𝕜]y] ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>h : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>openSegment 𝕜 x y ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<GOAL>Convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<GOAL>Convex 𝕜 ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<GOAL>Convex 𝕜 Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<GOAL>Convex 𝕜 (s ∩ t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>S : Set (Set E)<VAR>h : ∀ s ∈ S, Convex 𝕜 s<GOAL>Convex 𝕜 (⋂₀ S)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>ι : Sort u_5<VAR>s : ι → Set E<VAR>h : ∀ (i : ι), Convex 𝕜 (s i)<GOAL>Convex 𝕜 (⋂ i, s i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>s : (i : ι) → κ i → Set E<VAR>h : ∀ (i : ι) (j : κ i), Convex 𝕜 (s i j)<GOAL>Convex 𝕜 (⋂ i, ⋂ j, s i j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>SMul 𝕜 E<VAR>SMul 𝕜 F<VAR>s : Set E<VAR>t : Set F<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<GOAL>Convex 𝕜 (s ×ˢ t)
<VAR>𝕜 : Type u_1<VAR>OrderedSemiring 𝕜<VAR>ι : Type u_5<VAR>E : ι → Type u_6<VAR>(i : ι) → AddCommMonoid (E i)<VAR>(i : ι) → SMul 𝕜 (E i)<VAR>s : Set ι<VAR>t : (i : ι) → Set (E i)<VAR>ht : ∀ ⦃i : ι⦄, i ∈ s → Convex 𝕜 (t i)<GOAL>Convex 𝕜 (s.pi t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>ι : Sort u_5<VAR>s : ι → Set E<VAR>hdir : Directed (fun x x_1 => x ⊆ x_1) s<VAR>hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)<GOAL>Convex 𝕜 (⋃ i, s i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>c : Set (Set E)<VAR>hdir : DirectedOn (fun x x_1 => x ⊆ x_1) c<VAR>hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A<GOAL>Convex 𝕜 (⋃₀ c)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → openSegment 𝕜 x y ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>Convex 𝕜 s ↔ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : Convex 𝕜 s<VAR>h : s.Nonempty<GOAL>StarConvex 𝕜 x s ↔ x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>h : s.Subsingleton<GOAL>Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>c : E<GOAL>Convex 𝕜 {c}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<GOAL>Convex 𝕜 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x y : E<GOAL>Convex 𝕜 [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>f : E →ₗ[𝕜] F<GOAL>Convex 𝕜 (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>f : E → F<VAR>hf : IsLinearMap 𝕜 f<GOAL>Convex 𝕜 (f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set F<VAR>hs : Convex 𝕜 s<VAR>f : E →ₗ[𝕜] F<GOAL>Convex 𝕜 (⇑f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>AddCommMonoid F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set F<VAR>hs : Convex 𝕜 s<VAR>f : E → F<VAR>hf : IsLinearMap 𝕜 f<GOAL>Convex 𝕜 (f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<GOAL>Convex 𝕜 (s + t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<GOAL>↑(convexAddSubmonoid 𝕜 E) = {s | Convex 𝕜 s}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>s ∈ convexAddSubmonoid 𝕜 E ↔ Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>l : List (Set E)<VAR>h : ∀ i ∈ l, Convex 𝕜 i<GOAL>Convex 𝕜 l.sum
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Multiset (Set E)<VAR>h : ∀ i ∈ s, Convex 𝕜 i<GOAL>Convex 𝕜 s.sum
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>t : ι → Set E<VAR>h : ∀ i ∈ s, Convex 𝕜 (t i)<GOAL>Convex 𝕜 (∑ i ∈ s, t i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>z : E<GOAL>Convex 𝕜 (z +ᵥ s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>z : E<GOAL>Convex 𝕜 ((fun x => z + x) '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>z : E<GOAL>Convex 𝕜 ((fun x => z + x) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>z : E<GOAL>Convex 𝕜 ((fun x => x + z) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r : β<GOAL>Convex 𝕜 (Set.Iic r)
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r : β<GOAL>Convex 𝕜 (Set.Ici r)
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r s : β<GOAL>Convex 𝕜 (Set.Icc r s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : E → β<VAR>h : IsLinearMap 𝕜 f<VAR>r : β<GOAL>Convex 𝕜 {w | f w ≤ r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : E → β<VAR>h : IsLinearMap 𝕜 f<VAR>r : β<GOAL>Convex 𝕜 {w | r ≤ f w}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : E → β<VAR>h : IsLinearMap 𝕜 f<VAR>r : β<GOAL>Convex 𝕜 {w | f w = r}
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r : β<GOAL>Convex 𝕜 (Set.Iio r)
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r : β<GOAL>Convex 𝕜 (Set.Ioi r)
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r s : β<GOAL>Convex 𝕜 (Set.Ioo r s)
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r s : β<GOAL>Convex 𝕜 (Set.Ico r s)
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r s : β<GOAL>Convex 𝕜 (Set.Ioc r s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : E → β<VAR>h : IsLinearMap 𝕜 f<VAR>r : β<GOAL>Convex 𝕜 {w | f w < r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedCancelAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>f : E → β<VAR>h : IsLinearMap 𝕜 f<VAR>r : β<GOAL>Convex 𝕜 {w | r < f w}
<VAR>𝕜 : Type u_1<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r s : β<GOAL>Convex 𝕜 (Set.uIcc r s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : MonotoneOn f s<VAR>hs : Convex 𝕜 s<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ f x ≤ r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : MonotoneOn f s<VAR>hs : Convex 𝕜 s<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ f x < r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : MonotoneOn f s<VAR>hs : Convex 𝕜 s<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ r ≤ f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : MonotoneOn f s<VAR>hs : Convex 𝕜 s<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ r < f x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>β : Type u_4<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>OrderedAddCommMonoid β<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set E<VAR>f : E → β<VAR>hf : AntitoneOn f s<VAR>hs : Convex 𝕜 s<VAR>r : β<GOAL>Convex 𝕜 {x | x ∈ s ∧ f x ≤ r}