𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hAB : IsExposed 𝕜 A B
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ B ∧ x₂ ∈ B
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hAB : IsExposed 𝕜 A B
⊢ IsExtreme 𝕜 A B
refine' ⟨hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxB hx => _⟩
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hAB : IsExposed 𝕜 A B
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ B ∧ x₂ ∈ B
obtain ⟨l, rfl⟩ := hAB ⟨x, hxB⟩
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
have hl : ConvexOn 𝕜 univ l := l.toLinearMap.convexOn convex_univ
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
have hlx₁ := hxB.2 x₁ hx₁A
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
have hlx₂ := hxB.2 x₂ hx₂A
case intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x₁

case intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x₂
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
refine' ⟨⟨hx₁A, fun y hy => _⟩, ⟨hx₂A, fun y hy => _⟩⟩
case intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x
case intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x₁
rw [hlx₁.antisymm (hl.le_left_of_right_le (mem_univ _) (mem_univ _) hx hlx₂)]
no goals
case intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x
exact hxB.2 y hy
case intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x
case intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x₂
rw [hlx₂.antisymm (hl.le_right_of_left_le (mem_univ _) (mem_univ _) hx hlx₁)]
no goals
case intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x
exact hxB.2 y hy