α : Type u
β : Type v
γ : Type w
δ : Type ?u.279682
ι : Sort x
f : ι → Filter α
m : α → β
hf : Directed (fun x x_1 => x ≥ x_1) f
inst✝ : Nonempty ι
s : Set β
hs : m ⁻¹' s ∈ iInf f
i : ι
hi : m ⁻¹' s ∈ f i
⊢ m ⁻¹' s ∈ f i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.279682
ι : Sort x
f : ι → Filter α
m : α → β
hf : Directed (fun x x_1 => x ≥ x_1) f
inst✝ : Nonempty ι
s : Set β
hs : m ⁻¹' s ∈ iInf f
i : ι
hi : m ⁻¹' s ∈ f i
⊢ map m (f i) ≤ 𝓟 s
simp only [le_principal_iff, mem_map]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.279682
ι : Sort x
f : ι → Filter α
m : α → β
hf : Directed (fun x x_1 => x ≥ x_1) f
inst✝ : Nonempty ι
s : Set β
hs : m ⁻¹' s ∈ iInf f
i : ι
hi : m ⁻¹' s ∈ f i
⊢ m ⁻¹' s ∈ f i
assumption