ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>SMul 𝕜 E<VAR>s : Set E<VAR>x y : E<GOAL>[x-[𝕜]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>SMul 𝕜 E<VAR>s : Set E<VAR>x y : E<GOAL>openSegment 𝕜 x 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>MulActionWithZero 𝕜 E<VAR>x y : E<GOAL>x ∈ [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>MulActionWithZero 𝕜 E<VAR>x y : E<GOAL>y ∈ [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x : E<GOAL>[x-[𝕜]x] = {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x y : E<GOAL>insert x (insert y (openSegment 𝕜 x y)) = [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>x y z : E<VAR>hx : x ≠ z<VAR>hy : y ≠ z<VAR>hz : z ∈ [x-[𝕜]y]<GOAL>z ∈ openSegment 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>openSegment 𝕜 x y ⊆ s ↔ [x-[𝕜]y] ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Nontrivial 𝕜<VAR>DenselyOrdered 𝕜<VAR>x : E<GOAL>openSegment 𝕜 x x = {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<GOAL>[x-[𝕜]y] = (fun θ => (1 - θ) • x + θ • y) '' Set.Icc 0 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<GOAL>openSegment 𝕜 x y = (fun θ => (1 - θ) • x + θ • y) '' Set.Ioo 0 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<GOAL>[x-[𝕜]y] = (fun θ => x + θ • (y - x)) '' Set.Icc 0 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<GOAL>openSegment 𝕜 x y = (fun θ => x + θ • (y - x)) '' Set.Ioo 0 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<GOAL>[x-[𝕜]y] = ⇑(AffineMap.lineMap x y) '' Set.Icc 0 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<GOAL>openSegment 𝕜 x y = ⇑(AffineMap.lineMap x y) '' Set.Ioo 0 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>f : E →ᵃ[𝕜] F<VAR>a b : E<GOAL>⇑f '' [a-[𝕜]b] = [f a-[𝕜]f b]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>f : E →ᵃ[𝕜] F<VAR>a b : E<GOAL>⇑f '' openSegment 𝕜 a b = openSegment 𝕜 (f a) (f b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>G : Type u_4<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup G<VAR>Module 𝕜 E<VAR>AddTorsor G E<VAR>VAddCommClass G E E<VAR>a : G<VAR>b c : E<GOAL>a +ᵥ [b-[𝕜]c] = [a +ᵥ b-[𝕜]a +ᵥ c]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>G : Type u_4<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup G<VAR>Module 𝕜 E<VAR>AddTorsor G E<VAR>VAddCommClass G E E<VAR>a : G<VAR>b c : E<GOAL>a +ᵥ openSegment 𝕜 b c = openSegment 𝕜 (a +ᵥ b) (a +ᵥ c)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>a : E<VAR>x b c : E<GOAL>a + x ∈ [a + b-[𝕜]a + c] ↔ x ∈ [b-[𝕜]c]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>a : E<VAR>x b c : E<GOAL>a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>a b c : E<GOAL>(fun x => a + x) ⁻¹' [a + b-[𝕜]a + c] = [b-[𝕜]c]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>a b c : E<GOAL>(fun x => a + x) ⁻¹' openSegment 𝕜 (a + b) (a + c) = openSegment 𝕜 b c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>a b c : E<GOAL>(fun x => a + x) '' [b-[𝕜]c] = [a + b-[𝕜]a + c]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>a b c : E<GOAL>(fun x => a + x) '' openSegment 𝕜 b c = openSegment 𝕜 (a + b) (a + c)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>c x y : E<VAR>h : LinearIndependent 𝕜 ![x - c, y - c]<GOAL>[c-[𝕜]x] ∩ [c-[𝕜]y] = {c}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>StrictOrderedCommRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y z : E<VAR>h : x ∈ [y-[𝕜]z]<GOAL>SameRay 𝕜 (x - y) (z - x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedCommRing 𝕜<VAR>NoZeroDivisors 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<VAR>h : LinearIndependent 𝕜 ![x, y]<VAR>s t : 𝕜<VAR>hs : s ≠ t<VAR>c : E<GOAL>[c + x-[𝕜]c + t • y] ∩ [c + x-[𝕜]c + s • y] = {c + x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Invertible 2<VAR>x y : E<GOAL>midpoint 𝕜 x y ∈ [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Invertible 2<VAR>x y : E<GOAL>x ∈ [x - y-[𝕜]x + y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>Invertible 2<VAR>x y : E<GOAL>x ∈ [x + y-[𝕜]x - y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<VAR>DenselyOrdered 𝕜<VAR>NoZeroSMulDivisors 𝕜 E<GOAL>x ∈ openSegment 𝕜 x y ↔ x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedRing 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<VAR>DenselyOrdered 𝕜<VAR>NoZeroSMulDivisors 𝕜 E<GOAL>y ∈ openSegment 𝕜 x y ↔ x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedSemifield 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y z : E<GOAL>x ∈ [y-[𝕜]z] ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedSemifield 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y z : E<GOAL>x ∈ openSegment 𝕜 y z ↔ ∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y z : E<GOAL>x ∈ [y-[𝕜]z] ↔ SameRay 𝕜 (x - y) (z - x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>x y : E<VAR>z : E<VAR>hz : z ∈ Set.range ⇑(AffineMap.lineMap x y)<GOAL>openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedAddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>x y : E<VAR>h : x ≤ y<GOAL>[x-[𝕜]y] ⊆ Set.Icc x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>OrderedCancelAddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>x y : E<VAR>h : x < y<GOAL>openSegment 𝕜 x y ⊆ Set.Ioo x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>x y : E<GOAL>[x-[𝕜]y] ⊆ Set.uIcc x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>a b : 𝕜<VAR>x y : E<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>min x y ≤ a • x + b • y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>LinearOrderedAddCommMonoid E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>a b : 𝕜<VAR>x y : E<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • x + b • y ≤ max x y
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x y : 𝕜<GOAL>Set.Icc x y ⊆ [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x y : 𝕜<VAR>h : x ≤ y<GOAL>[x-[𝕜]y] = Set.Icc x y
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x y : 𝕜<GOAL>Set.Ioo x y ⊆ openSegment 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x y : 𝕜<VAR>h : x < y<GOAL>openSegment 𝕜 x y = Set.Ioo x y
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x y : 𝕜<GOAL>[x-[𝕜]y] = Set.Icc (min x y) (max x y)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x y : 𝕜<VAR>hxy : x ≠ y<GOAL>openSegment 𝕜 x y = Set.Ioo (min x y) (max x y)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x y : 𝕜<GOAL>[x-[𝕜]y] = Set.uIcc x y
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x y z : 𝕜<VAR>h : x ≤ y<GOAL>z ∈ Set.Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x y z : 𝕜<VAR>h : x < y<GOAL>z ∈ Set.Ioo x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x y z : 𝕜<VAR>h : x < y<GOAL>z ∈ Set.Ioc x y ↔ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>x y z : 𝕜<VAR>h : x < y<GOAL>z ∈ Set.Ico x y ↔ ∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z
<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>x y : E × F<GOAL>[x-[𝕜]y] ⊆ [x.1-[𝕜]y.1] ×ˢ [x.2-[𝕜]y.2]
<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>x y : E × F<GOAL>openSegment 𝕜 x y ⊆ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2
<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>x₁ x₂ : E<VAR>y : F<GOAL>(fun x => (x, y)) '' [x₁-[𝕜]x₂] = [(x₁, y)-[𝕜](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>x : E<VAR>y₁ y₂ : F<GOAL>(fun y => (x, y)) '' [y₁-[𝕜]y₂] = [(x, y₁)-[𝕜](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>x₁ x₂ : E<VAR>y : F<GOAL>(fun x => (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (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>x : E<VAR>y₁ y₂ : F<GOAL>(fun y => (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>OrderedSemiring 𝕜<VAR>(i : ι) → AddCommMonoid (π i)<VAR>(i : ι) → Module 𝕜 (π i)<VAR>s : Set ι<VAR>x y : (i : ι) → π i<GOAL>[x-[𝕜]y] ⊆ s.pi fun i => [x i-[𝕜]y i]
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>OrderedSemiring 𝕜<VAR>(i : ι) → AddCommMonoid (π i)<VAR>(i : ι) → Module 𝕜 (π i)<VAR>s : Set ι<VAR>x y : (i : ι) → π i<GOAL>openSegment 𝕜 x y ⊆ s.pi fun i => openSegment 𝕜 (x i) (y i)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>OrderedSemiring 𝕜<VAR>(i : ι) → AddCommMonoid (π i)<VAR>(i : ι) → Module 𝕜 (π i)<VAR>DecidableEq ι<VAR>i : ι<VAR>x₁ x₂ : π i<VAR>y : (i : ι) → π i<GOAL>Function.update y i '' [x₁-[𝕜]x₂] = [Function.update y i x₁-[𝕜]Function.update y i x₂]
<VAR>𝕜 : Type u_1<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>OrderedSemiring 𝕜<VAR>(i : ι) → AddCommMonoid (π i)<VAR>(i : ι) → Module 𝕜 (π i)<VAR>DecidableEq ι<VAR>i : ι<VAR>x₁ x₂ : π i<VAR>y : (i : ι) → π i<GOAL>Function.update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (Function.update y i x₁) (Function.update y i x₂)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<GOAL>ConvexOn ℝ s norm
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<GOAL>ConvexOn ℝ Set.univ norm
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>z : E<VAR>hs : Convex ℝ s<GOAL>ConvexOn ℝ s fun z' => dist z' z
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>z : E<GOAL>ConvexOn ℝ Set.univ fun z' => dist z' z
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : E<VAR>r : ℝ<GOAL>Convex ℝ (Metric.ball a r)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : E<VAR>r : ℝ<GOAL>Convex ℝ (Metric.closedBall a r)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>δ : ℝ<GOAL>Convex ℝ (Metric.thickening δ s)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>δ : ℝ<GOAL>Convex ℝ (Metric.cthickening δ s)
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull ℝ) s<VAR>y : E<GOAL>∃ x' ∈ s, dist x y ≤ dist x' y
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hx : x ∈ (convexHull ℝ) s<VAR>hy : y ∈ (convexHull ℝ) t<GOAL>∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<GOAL>EMetric.diam ((convexHull ℝ) s) = EMetric.diam s
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<GOAL>Metric.diam ((convexHull ℝ) s) = Metric.diam s
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<GOAL>Bornology.IsBounded ((convexHull ℝ) s) ↔ Bornology.IsBounded s
<VAR>E : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>x y z : P<VAR>h : Wbtw ℝ x y z<GOAL>dist x y + dist y z = dist x z
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x y z : E<VAR>h : y ∈ [x-[ℝ]z]<GOAL>dist x y + dist y z = dist x z
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : E<GOAL>IsConnected {y | SameRay ℝ x y}
<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : E<VAR>hx : x ≠ 0<GOAL>IsConnected {y | SameRay ℝ x y ∧ y ≠ 0}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>f : E → ℝ<GOAL>UniformConvexOn s 0 f ↔ ConvexOn ℝ s f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>f : E → ℝ<GOAL>UniformConcaveOn s 0 f ↔ ConcaveOn ℝ s f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>f : E → ℝ<VAR>hψφ : ψ ≤ φ<VAR>hf : UniformConvexOn s φ f<GOAL>UniformConvexOn s ψ f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>f : E → ℝ<VAR>hψφ : ψ ≤ φ<VAR>hf : UniformConcaveOn s φ f<GOAL>UniformConcaveOn s ψ f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ : ℝ → ℝ<VAR>s : Set E<VAR>f : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>hφ : 0 ≤ φ<GOAL>ConvexOn ℝ s f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ : ℝ → ℝ<VAR>s : Set E<VAR>f : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hφ : 0 ≤ φ<GOAL>ConcaveOn ℝ s f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ : ℝ → ℝ<VAR>s : Set E<VAR>f : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r<GOAL>StrictConvexOn ℝ s f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ : ℝ → ℝ<VAR>s : Set E<VAR>f : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r<GOAL>StrictConcaveOn ℝ s f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>f g : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>hg : UniformConvexOn s ψ g<GOAL>UniformConvexOn s (φ + ψ) (f + g)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hg : UniformConcaveOn s ψ g<GOAL>UniformConcaveOn s (φ + ψ) (f + g)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ : ℝ → ℝ<VAR>s : Set E<VAR>f : E → ℝ<VAR>hf : UniformConvexOn s φ f<GOAL>UniformConcaveOn s φ (-f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ : ℝ → ℝ<VAR>s : Set E<VAR>f : E → ℝ<VAR>hf : UniformConcaveOn s φ f<GOAL>UniformConvexOn s φ (-f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>f g : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>hg : UniformConcaveOn s ψ g<GOAL>UniformConvexOn s (φ + ψ) (f - g)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hg : UniformConvexOn s ψ g<GOAL>UniformConcaveOn s (φ + ψ) (f - g)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>f : E → ℝ<VAR>m n : ℝ<VAR>hmn : m ≤ n<VAR>hf : StrongConvexOn s n f<GOAL>StrongConvexOn s m f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>f : E → ℝ<VAR>m n : ℝ<VAR>hmn : m ≤ n<VAR>hf : StrongConcaveOn s n f<GOAL>StrongConcaveOn s m f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>f : E → ℝ<GOAL>StrongConvexOn s 0 f ↔ ConvexOn ℝ s f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>f : E → ℝ<GOAL>StrongConcaveOn s 0 f ↔ ConcaveOn ℝ s f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>f : E → ℝ<VAR>m : ℝ<VAR>hf : StrongConvexOn s m f<VAR>hm : 0 < m<GOAL>StrictConvexOn ℝ s f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>f : E → ℝ<VAR>m : ℝ<VAR>hf : StrongConcaveOn s m f<VAR>hm : 0 < m<GOAL>StrictConcaveOn ℝ s f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>a b m : ℝ<VAR>x y : E<VAR>f : E → ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) + m / 2 * ‖a • x + b • y‖ ^ 2 = a * f x + b * f y - m / 2 * a * b * ‖x - y‖ ^ 2
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>a b m : ℝ<VAR>x y : E<VAR>f : E → ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a * (f x + m / 2 * ‖x‖ ^ 2) + b * (f y + m / 2 * ‖y‖ ^ 2) - m / 2 * ‖a • x + b • y‖ ^ 2 = a * f x + b * f y + m / 2 * a * b * ‖x - y‖ ^ 2
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>s : Set E<VAR>m : ℝ<VAR>f : E → ℝ<GOAL>StrongConvexOn s m f ↔ ConvexOn ℝ s fun x => f x - m / 2 * ‖x‖ ^ 2
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>s : Set E<VAR>m : ℝ<VAR>f : E → ℝ<GOAL>StrongConcaveOn s m f ↔ ConcaveOn ℝ s fun x => f x + m / 2 * ‖x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A : Set E<GOAL>IsExposed 𝕜 A (l.toExposed A)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A : Set E<GOAL>IsExposed 𝕜 A ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A B : Set E<VAR>hAB : IsExposed 𝕜 A B<GOAL>B ⊆ A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A : Set E<GOAL>IsExposed 𝕜 A A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A B : Set E<VAR>hB : IsExposed 𝕜 A B<VAR>hA : IsExposed 𝕜 B A<GOAL>A = B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A B C : Set E<VAR>hC : IsExposed 𝕜 A C<VAR>hBA : B ⊆ A<VAR>hCB : C ⊆ B<GOAL>IsExposed 𝕜 B C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A B : Set E<VAR>hAB : IsExposed 𝕜 A B<VAR>hB : B.Nonempty<GOAL>∃ l a, B = {x | x ∈ A ∧ a ≤ l x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>Nontrivial 𝕜<VAR>A B : Set E<VAR>hAB : IsExposed 𝕜 A B<GOAL>∃ l a, B = {x | x ∈ A ∧ a ≤ l x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>ContinuousAdd 𝕜<VAR>A B C : Set E<VAR>hB : IsExposed 𝕜 A B<VAR>hC : IsExposed 𝕜 A C<GOAL>IsExposed 𝕜 A (B ∩ C)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>ContinuousAdd 𝕜<VAR>F : Finset (Set E)<VAR>hF : F.Nonempty<VAR>hAF : ∀ B ∈ F, IsExposed 𝕜 A B<GOAL>IsExposed 𝕜 A (⋂₀ ↑F)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A B C : Set E<VAR>hC : IsExposed 𝕜 A C<VAR>hCB : C ⊆ B<GOAL>IsExposed 𝕜 (A ∩ B) C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A B C : Set E<VAR>hC : IsExposed 𝕜 B C<VAR>hCA : C ⊆ A<GOAL>IsExposed 𝕜 (A ∩ B) C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>OrderClosedTopology 𝕜<VAR>A B : Set E<VAR>hAB : IsExposed 𝕜 A B<VAR>hA : IsClosed A<GOAL>IsClosed B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>OrderClosedTopology 𝕜<VAR>T2Space E<VAR>A B : Set E<VAR>hAB : IsExposed 𝕜 A B<VAR>hA : IsCompact A<GOAL>IsCompact B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>x : E<GOAL>x ∈ Set.exposedPoints 𝕜 A ↔ x ∈ A ∧ ∃ l, ∀ y ∈ A, l y ≤ l x ∧ (l x ≤ l y → y = x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A : Set E<GOAL>Set.exposedPoints 𝕜 A ⊆ A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<GOAL>Set.exposedPoints 𝕜 ∅ = ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>OrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A : Set E<VAR>x : E<GOAL>x ∈ Set.exposedPoints 𝕜 A ↔ IsExposed 𝕜 A {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>LinearOrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A B : Set E<VAR>hAB : IsExposed 𝕜 A B<VAR>hA : Convex 𝕜 A<GOAL>Convex 𝕜 B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>LinearOrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A B : Set E<VAR>hAB : IsExposed 𝕜 A B<GOAL>IsExtreme 𝕜 A B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>TopologicalSpace 𝕜<VAR>LinearOrderedRing 𝕜<VAR>AddCommMonoid E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>A : Set E<GOAL>Set.exposedPoints 𝕜 A ⊆ Set.extremePoints 𝕜 A
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<GOAL>gauge s x = sInf {r | r ∈ Set.Ioi 0 ∧ x ∈ r • s}
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<GOAL>gauge s x = sInf {r | r ∈ Set.Ioi 0 ∧ r⁻¹ • x ∈ s}
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<GOAL>BddBelow {r | 0 < r ∧ x ∈ r • s}
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>absorbs : Absorbent ℝ s<GOAL>{r | 0 < r ∧ x ∈ r • s}.Nonempty
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s t : Set E<VAR>hs : Absorbent ℝ s<VAR>h : s ⊆ t<GOAL>gauge t ≤ gauge s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>a : ℝ<VAR>absorbs : Absorbent ℝ s<VAR>h : gauge s x < a<GOAL>∃ b, 0 < b ∧ b < a ∧ x ∈ b • s
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<GOAL>gauge s 0 = 0
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<GOAL>gauge 0 = 0
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<GOAL>gauge ∅ = 0
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>h : s ⊆ 0<GOAL>gauge s = 0
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<GOAL>0 ≤ gauge s x
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>symmetric : ∀ x ∈ s, -x ∈ s<VAR>x : E<GOAL>gauge s (-x) = gauge s x
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<GOAL>gauge (-s) (-x) = gauge s x
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<GOAL>gauge (-s) x = gauge s (-x)
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : Set E<VAR>x : E<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>hx : x ∈ a • s<GOAL>gauge s x ≤ a