α : Type u_1
β : Type ?u.9938
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t s : Set α
⊢ (∀ (x x_1 : { a // ↑toDual a ∈ ↑ofDual ⁻¹' s }), ↑ofDual ⁻¹' Icc ↑x_1 ↑x ⊆ ↑ofDual ⁻¹' s) ↔
    ∀ (x x_1 : { a // a ∈ s }), Icc ↑x ↑x_1 ⊆ s
α : Type u_1
β : Type ?u.9938
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t s : Set α
⊢ OrdConnected (↑ofDual ⁻¹' s) ↔ OrdConnected s
simp_rw [ordConnected_def, toDual.surjective.forall, dual_Icc, Subtype.forall']
no goals
α : Type u_1
β : Type ?u.9938
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t s : Set α
⊢ (∀ (x x_1 : { a // ↑toDual a ∈ ↑ofDual ⁻¹' s }), ↑ofDual ⁻¹' Icc ↑x_1 ↑x ⊆ ↑ofDual ⁻¹' s) ↔
    ∀ (x x_1 : { a // a ∈ s }), Icc ↑x ↑x_1 ⊆ s
exact forall_swap