α : Type u_1
β : Type ?u.113900
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioo (↑toDual a) (↑toDual b) = Ioo b a
α : Type u_1
β : Type ?u.113900
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioo (↑toDual a) (↑toDual b) = map (Equiv.toEmbedding toDual) (Ioo b a)
refine' Eq.trans _ map_refl.symm
case a
α : Type u_1
β : Type ?u.113900
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ c ∈ Ioo (↑toDual a) (↑toDual b) ↔ c ∈ Ioo b a
α : Type u_1
β : Type ?u.113900
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioo (↑toDual a) (↑toDual b) = Ioo b a
ext c
case a
α : Type u_1
β : Type ?u.113900
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ ↑toDual a < c ∧ c < ↑toDual b ↔ b < c ∧ c < a
case a
α : Type u_1
β : Type ?u.113900
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ c ∈ Ioo (↑toDual a) (↑toDual b) ↔ c ∈ Ioo b a
rw [mem_Ioo, mem_Ioo (α := α)]
no goals
case a
α : Type u_1
β : Type ?u.113900
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ ↑toDual a < c ∧ c < ↑toDual b ↔ b < c ∧ c < a
exact and_comm