apply inter_subset_right
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
x : α
hx : x ∈ s
⊢ {x_1 | f x_1 ≤ f x} ∈ φ (f x)
no goals