α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.18544
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (sSup (range f)))
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.18544
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (range (l ∘ f)) (l (iSup f))
rw [range_comp, ← sSup_range]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.18544
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (sSup (range f)))
exact gc.isLUB_l_image (isLUB_sSup _)