𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.3511
ι : Type ?u.3514
π : ι → Type ?u.3519
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
F : Set (Set E)
hF : Set.Nonempty F
hA : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
this : Nonempty ↑F
⊢ IsExtreme 𝕜 A (⋂ (B : Set E) (_ : B ∈ F), B)
𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.3511
ι : Type ?u.3514
π : ι → Type ?u.3519
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
F : Set (Set E)
hF : Set.Nonempty F
hA : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
⊢ IsExtreme 𝕜 A (⋂ (B : Set E) (_ : B ∈ F), B)
haveI := hF.to_subtype
no goals
𝕜 : Type u_2
E : Type u_1
F✝ : Type ?u.3511
ι : Type ?u.3514
π : ι → Type ?u.3519
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
x : E
F : Set (Set E)
hF : Set.Nonempty F
hA : ∀ (B : Set E), B ∈ F → IsExtreme 𝕜 A B
this : Nonempty ↑F
⊢ IsExtreme 𝕜 A (⋂ (B : Set E) (_ : B ∈ F), B)
simpa only [iInter_subtype] using isExtreme_iInter fun i : F ↦ hA _ i.2