α : Type u_1
β : Type u_2
γ : Type ?u.4510
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ↑fa ↑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB {x | g x ≤ ↑fb y} (↑fa (g' y))
α : Type u_1
β : Type u_2
γ : Type ?u.4510
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ↑fa ↑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
⊢ Semiconj g' ↑fb ↑fa
refine' fun y => (hg' _).unique _
α : Type u_1
β : Type u_2
γ : Type ?u.4510
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ↑fa ↑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB (↑fa '' {a | g (↑fa a) ≤ ↑fb y}) (↑fa (g' y))
α : Type u_1
β : Type u_2
γ : Type ?u.4510
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ↑fa ↑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB {x | g x ≤ ↑fb y} (↑fa (g' y))
rw [← fa.surjective.image_preimage { x | g x ≤ fb y }, preimage_setOf_eq]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.4510
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ↑fa ↑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB (↑fa '' {a | g (↑fa a) ≤ ↑fb y}) (↑fa (g' y))
simp only [h.eq, fb.le_iff_le, fa.leftOrdContinuous (hg' _)]