α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddBelow s
⊢ sSup (Inv.inv '' s) = (sInf s)⁻¹
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddBelow s
⊢ sSup s⁻¹ = (sInf s)⁻¹
rw [← image_inv]
no goals
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddBelow s
⊢ sSup (Inv.inv '' s) = (sInf s)⁻¹
exact ((OrderIso.inv α).map_csInf' hs₀ hs₁).symm