α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ((⨅ (b : α) (_ : b ∈ Iio a), 𝓟 (Ioi b)) ⊓ ⨅ (b : α) (_ : b ∈ Ioi a), 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) =
    (⨅ (u : α) (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[Ici a] a = (⨅ (u : α) (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
rw [nhdsWithin, nhds_eq_order]
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ (⨅ (u : α) (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) ≤ ⨅ (b : α) (_ : b ∈ Iio a), 𝓟 (Ioi b)
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ((⨅ (b : α) (_ : b ∈ Iio a), 𝓟 (Ioi b)) ⊓ ⨅ (b : α) (_ : b ∈ Ioi a), 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) =
    (⨅ (u : α) (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
refine' le_antisymm (inf_le_inf_right _ inf_le_right) (le_inf (le_inf _ inf_le_left) inf_le_right)
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ (⨅ (u : α) (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) ≤ ⨅ (b : α) (_ : b ∈ Iio a), 𝓟 (Ioi b)
exact inf_le_right.trans (le_iInf₂ fun l hl => principal_mono.2 <| Ici_subset_Ioi.2 hl)