case intro
𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.4264
ι : Type ?u.4267
π : ι → Type ?u.4272
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B✝ C : Set E
x : E
F : Set (Set E)
hAF : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
B : Set E
hB : B ∈ F
⊢ IsExtreme 𝕜 A (⋂₀ F)
𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.4264
ι : Type ?u.4267
π : ι → Type ?u.4272
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
F : Set (Set E)
hF : Set.Nonempty F
hAF : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
⊢ IsExtreme 𝕜 A (⋂₀ F)
obtain ⟨B, hB⟩ := hF
case intro
𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.4264
ι : Type ?u.4267
π : ι → Type ?u.4272
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B✝ C : Set E
x✝ : E
F : Set (Set E)
hAF : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
B : Set E
hB : B ∈ F
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxF : x ∈ ⋂₀ F
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ ⋂₀ F ∧ x₂ ∈ ⋂₀ F
case intro
𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.4264
ι : Type ?u.4267
π : ι → Type ?u.4272
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B✝ C : Set E
x : E
F : Set (Set E)
hAF : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
B : Set E
hB : B ∈ F
⊢ IsExtreme 𝕜 A (⋂₀ F)
refine' ⟨(sInter_subset_of_mem hB).trans (hAF B hB).1, fun x₁ hx₁A x₂ hx₂A x hxF hx ↦ _⟩
case intro
𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.4264
ι : Type ?u.4267
π : ι → Type ?u.4272
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B✝ C : Set E
x✝ : E
F : Set (Set E)
hAF : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
B : Set E
hB : B ∈ F
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
hxF : ∀ (t : Set E), t ∈ F → x ∈ t
⊢ (∀ (t : Set E), t ∈ F → x₁ ∈ t) ∧ ∀ (t : Set E), t ∈ F → x₂ ∈ t
case intro
𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.4264
ι : Type ?u.4267
π : ι → Type ?u.4272
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B✝ C : Set E
x✝ : E
F : Set (Set E)
hAF : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
B : Set E
hB : B ∈ F
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxF : x ∈ ⋂₀ F
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ ⋂₀ F ∧ x₂ ∈ ⋂₀ F
simp_rw [mem_sInter] at hxF⊢
case intro
𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.4264
ι : Type ?u.4267
π : ι → Type ?u.4272
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B✝ C : Set E
x✝ : E
F : Set (Set E)
hAF : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
B : Set E
hB : B ∈ F
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
hxF : ∀ (t : Set E), t ∈ F → x ∈ t
h : ∀ (B : Set E), B ∈ F → x₁ ∈ B ∧ x₂ ∈ B
⊢ (∀ (t : Set E), t ∈ F → x₁ ∈ t) ∧ ∀ (t : Set E), t ∈ F → x₂ ∈ t
case intro
𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.4264
ι : Type ?u.4267
π : ι → Type ?u.4272
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B✝ C : Set E
x✝ : E
F : Set (Set E)
hAF : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
B : Set E
hB : B ∈ F
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
hxF : ∀ (t : Set E), t ∈ F → x ∈ t
⊢ (∀ (t : Set E), t ∈ F → x₁ ∈ t) ∧ ∀ (t : Set E), t ∈ F → x₂ ∈ t
have h := fun B hB ↦ (hAF B hB).2 hx₁A hx₂A (hxF B hB) hx
no goals
case intro
𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.4264
ι : Type ?u.4267
π : ι → Type ?u.4272
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B✝ C : Set E
x✝ : E
F : Set (Set E)
hAF : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
B : Set E
hB : B ∈ F
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
hxF : ∀ (t : Set E), t ∈ F → x ∈ t
h : ∀ (B : Set E), B ∈ F → x₁ ∈ B ∧ x₂ ∈ B
⊢ (∀ (t : Set E), t ∈ F → x₁ ∈ t) ∧ ∀ (t : Set E), t ∈ F → x₂ ∈ t
exact ⟨fun B hB ↦ (h B hB).1, fun B hB ↦ (h B hB).2⟩