α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
⊢ ↑ofDual ⁻¹' [[x✝, x]] ⊆ ↑ofDual ⁻¹' s ↔ ↑toDual x ∈ ↑ofDual ⁻¹' ordConnectedComponent s x✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
⊢ ↑toDual x ∈ ordConnectedComponent (↑ofDual ⁻¹' s) (↑toDual x✝) ↔ ↑toDual x ∈ ↑ofDual ⁻¹' ordConnectedComponent s x✝
rw [mem_ordConnectedComponent, dual_uIcc]
no goals
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
⊢ ↑ofDual ⁻¹' [[x✝, x]] ⊆ ↑ofDual ⁻¹' s ↔ ↑toDual x ∈ ↑ofDual ⁻¹' ordConnectedComponent s x✝
rfl