ι : Sort ?u.15181
α : Type u_1
β : Type ?u.15187
X : Type ?u.15190
Y : Type ?u.15193
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ l₁ ≤ l₂
ι : Sort ?u.15181
α : Type u_1
β : Type ?u.15187
X : Type ?u.15190
Y : Type ?u.15193
l₁ l₂ : Filter α
⊢ 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂
refine' ⟨fun h => _, fun h => monotone_nhds h⟩
ι : Sort ?u.15181
α : Type u_1
β : Type ?u.15187
X : Type ?u.15190
Y : Type ?u.15193
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ ⋂₀ {s | s ∈ 𝓝 l₁} ⊆ ⋂₀ {s | s ∈ 𝓝 l₂}
ι : Sort ?u.15181
α : Type u_1
β : Type ?u.15187
X : Type ?u.15190
Y : Type ?u.15193
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ l₁ ≤ l₂
rw [← Iic_subset_Iic, ← sInter_nhds, ← sInter_nhds]
no goals
ι : Sort ?u.15181
α : Type u_1
β : Type ?u.15187
X : Type ?u.15190
Y : Type ?u.15193
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ ⋂₀ {s | s ∈ 𝓝 l₁} ⊆ ⋂₀ {s | s ∈ 𝓝 l₂}
exact sInter_subset_sInter h