𝕜 : Type ?u.130888
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s ∧ ↑i x ≤ ↑i y} = s
𝕜 : Type ?u.130888
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ (⋂ (l : E →L[ℝ] ℝ), {x | ∃ y, y ∈ s ∧ ↑l x ≤ ↑l y}) = s
rw [Set.iInter_setOf]
𝕜 : Type ?u.130888
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s ∧ ↑i x ≤ ↑i y}
⊢ x ∈ s
𝕜 : Type ?u.130888
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s ∧ ↑i x ≤ ↑i y} = s
refine' Set.Subset.antisymm (fun x hx => _) fun x hx l => ⟨x, hx, le_rfl⟩
𝕜 : Type ?u.130888
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s ∧ ↑i x ≤ ↑i y}
h : ¬x ∈ s
⊢ False
𝕜 : Type ?u.130888
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s ∧ ↑i x ≤ ↑i y}
⊢ x ∈ s
by_contra h
case intro.intro.intro
𝕜 : Type ?u.130888
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s✝ t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s✝ ∧ ↑i x ≤ ↑i y}
h : ¬x ∈ s✝
l : E →L[ℝ] ℝ
s : ℝ
hlA : ∀ (a : E), a ∈ s✝ → ↑l a < s
hl : s < ↑l x
⊢ False
𝕜 : Type ?u.130888
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s ∧ ↑i x ≤ ↑i y}
h : ¬x ∈ s
⊢ False
obtain ⟨l, s, hlA, hl⟩ := geometric_hahn_banach_closed_point hs₁ hs₂ h
case intro.intro.intro.intro.intro
𝕜 : Type ?u.130888
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s✝ t : Set E
x✝ y✝ : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s✝ ∧ ↑i x ≤ ↑i y}
h : ¬x ∈ s✝
l : E →L[ℝ] ℝ
s : ℝ
hlA : ∀ (a : E), a ∈ s✝ → ↑l a < s
hl : s < ↑l x
y : E
hy : y ∈ s✝
hxy : ↑l x ≤ ↑l y
⊢ False
case intro.intro.intro
𝕜 : Type ?u.130888
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s✝ t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s✝ ∧ ↑i x ≤ ↑i y}
h : ¬x ∈ s✝
l : E →L[ℝ] ℝ
s : ℝ
hlA : ∀ (a : E), a ∈ s✝ → ↑l a < s
hl : s < ↑l x
⊢ False
obtain ⟨y, hy, hxy⟩ := hx l
no goals
case intro.intro.intro.intro.intro
𝕜 : Type ?u.130888
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s✝ t : Set E
x✝ y✝ : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s✝ ∧ ↑i x ≤ ↑i y}
h : ¬x ∈ s✝
l : E →L[ℝ] ℝ
s : ℝ
hlA : ∀ (a : E), a ∈ s✝ → ↑l a < s
hl : s < ↑l x
y : E
hy : y ∈ s✝
hxy : ↑l x ≤ ↑l y
⊢ False
exact ((hxy.trans_lt (hlA y hy)).trans hl).not_le le_rfl