α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, ↑toDual a < ↑toDual u ∧ ↑ofDual ⁻¹' Icc u a ⊆ ↑ofDual ⁻¹' s) ↔ ∃ l, l < a ∧ Icc l a ⊆ s
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, ↑toDual a < ↑toDual u ∧ Icc (↑toDual a) (↑toDual u) ⊆ ↑ofDual ⁻¹' s) ↔ ∃ l, l < a ∧ Icc l a ⊆ s
simp only [dual_Icc]
no goals
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, ↑toDual a < ↑toDual u ∧ ↑ofDual ⁻¹' Icc u a ⊆ ↑ofDual ⁻¹' s) ↔ ∃ l, l < a ∧ Icc l a ⊆ s
rfl