𝕜 : Type u_3
E : Type u_2
F✝ : Type ?u.2902
ι✝ : Type ?u.2905
π : ι✝ → Type ?u.2910
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A B C : Set E
x : E
ι : Sort u_1
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
i : ι
⊢ IsExtreme 𝕜 A (⋂ (i : ι), F i)
𝕜 : Type u_3
E : Type u_2
F✝ : Type ?u.2902
ι✝ : Type ?u.2905
π : ι✝ → Type ?u.2910
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A B C : Set E
x : E
ι : Sort u_1
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
⊢ IsExtreme 𝕜 A (⋂ (i : ι), F i)
obtain i := Classical.arbitrary ι
𝕜 : Type u_3
E : Type u_2
F✝ : Type ?u.2902
ι✝ : Type ?u.2905
π : ι✝ → Type ?u.2910
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A B C : Set E
x✝ : E
ι : Sort u_1
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
i : ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxF : x ∈ ⋂ (i : ι), F i
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ (x₁ ∈ ⋂ (i : ι), F i) ∧ x₂ ∈ ⋂ (i : ι), F i
𝕜 : Type u_3
E : Type u_2
F✝ : Type ?u.2902
ι✝ : Type ?u.2905
π : ι✝ → Type ?u.2910
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A B C : Set E
x : E
ι : Sort u_1
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
i : ι
⊢ IsExtreme 𝕜 A (⋂ (i : ι), F i)
refine' ⟨iInter_subset_of_subset i (hAF i).1, fun x₁ hx₁A x₂ hx₂A x hxF hx ↦ _⟩
𝕜 : Type u_3
E : Type u_2
F✝ : Type ?u.2902
ι✝ : Type ?u.2905
π : ι✝ → Type ?u.2910
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A B C : Set E
x✝ : E
ι : Sort u_1
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
i : ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
hxF : ∀ (i : ι), x ∈ F i
⊢ (∀ (i : ι), x₁ ∈ F i) ∧ ∀ (i : ι), x₂ ∈ F i
𝕜 : Type u_3
E : Type u_2
F✝ : Type ?u.2902
ι✝ : Type ?u.2905
π : ι✝ → Type ?u.2910
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A B C : Set E
x✝ : E
ι : Sort u_1
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
i : ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxF : x ∈ ⋂ (i : ι), F i
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ (x₁ ∈ ⋂ (i : ι), F i) ∧ x₂ ∈ ⋂ (i : ι), F i
simp_rw [mem_iInter] at hxF⊢
𝕜 : Type u_3
E : Type u_2
F✝ : Type ?u.2902
ι✝ : Type ?u.2905
π : ι✝ → Type ?u.2910
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A B C : Set E
x✝ : E
ι : Sort u_1
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
i : ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
hxF : ∀ (i : ι), x ∈ F i
h : ∀ (i : ι), x₁ ∈ F i ∧ x₂ ∈ F i
⊢ (∀ (i : ι), x₁ ∈ F i) ∧ ∀ (i : ι), x₂ ∈ F i
𝕜 : Type u_3
E : Type u_2
F✝ : Type ?u.2902
ι✝ : Type ?u.2905
π : ι✝ → Type ?u.2910
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A B C : Set E
x✝ : E
ι : Sort u_1
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
i : ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
hxF : ∀ (i : ι), x ∈ F i
⊢ (∀ (i : ι), x₁ ∈ F i) ∧ ∀ (i : ι), x₂ ∈ F i
have h := fun i ↦ (hAF i).2 hx₁A hx₂A (hxF i) hx
no goals
𝕜 : Type u_3
E : Type u_2
F✝ : Type ?u.2902
ι✝ : Type ?u.2905
π : ι✝ → Type ?u.2910
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A B C : Set E
x✝ : E
ι : Sort u_1
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
i : ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
hxF : ∀ (i : ι), x ∈ F i
h : ∀ (i : ι), x₁ ∈ F i ∧ x₂ ∈ F i
⊢ (∀ (i : ι), x₁ ∈ F i) ∧ ∀ (i : ι), x₂ ∈ F i
exact ⟨fun i ↦ (h i).1, fun i ↦ (h i).2⟩