α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
this : ↑ofDual ⁻¹' s ∈ 𝓝[Ioi (↑toDual a)] ↑toDual a ↔ ∃ u, u ∈ Ioi (↑toDual a) ∧ Ioc (↑toDual a) u ⊆ ↑ofDual ⁻¹' s
⊢ s ∈ 𝓝[Iio a] a ↔ ∃ l, l ∈ Iio a ∧ Ico l a ⊆ s
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[Iio a] a ↔ ∃ l, l ∈ Iio a ∧ Ico l a ⊆ s
have : ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ _ := mem_nhdsWithin_Ioi_iff_exists_Ioc_subset
no goals
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
this : ↑ofDual ⁻¹' s ∈ 𝓝[Ioi (↑toDual a)] ↑toDual a ↔ ∃ u, u ∈ Ioi (↑toDual a) ∧ Ioc (↑toDual a) u ⊆ ↑ofDual ⁻¹' s
⊢ s ∈ 𝓝[Iio a] a ↔ ∃ l, l ∈ Iio a ∧ Ico l a ⊆ s
simpa only [OrderDual.exists, exists_prop, dual_Ioc] using this