case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
hA : Convex 𝕜 A
hAB : IsExposed 𝕜 A ∅
⊢ Convex 𝕜 ∅

case inr
𝕜 : 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
hA : Convex 𝕜 A
hB : Set.Nonempty B
⊢ Convex 𝕜 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
hA : Convex 𝕜 A
⊢ Convex 𝕜 B
obtain rfl | hB := B.eq_empty_or_nonempty
case inr.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
hA : Convex 𝕜 A
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hB : Set.Nonempty {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ Convex 𝕜 {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
case inr
𝕜 : 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
hA : Convex 𝕜 A
hB : Set.Nonempty B
⊢ Convex 𝕜 B
obtain ⟨l, rfl⟩ := hAB hB
no goals
case inr.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
hA : Convex 𝕜 A
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hB : Set.Nonempty {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ Convex 𝕜 {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
exact fun x₁ hx₁ x₂ hx₂ a b ha hb hab =>
  ⟨hA hx₁.1 hx₂.1 ha hb hab, fun y hy =>
    ((l.toLinearMap.concaveOn convex_univ).convex_ge _ ⟨mem_univ _, hx₁.2 y hy⟩
        ⟨mem_univ _, hx₂.2 y hy⟩ ha hb hab).2⟩
no goals
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
hA : Convex 𝕜 A
hAB : IsExposed 𝕜 A ∅
⊢ Convex 𝕜 ∅
exact convex_empty