α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.100664
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : Set.Nonempty s
this : Nonempty ↑s
⊢ l (⨆ (i : ↑s), f ↑i) = ⨆ (i : ↑s), l (f ↑i)
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.100664
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : Set.Nonempty s
⊢ l (⨆ (i : ↑s), f ↑i) = ⨆ (i : ↑s), l (f ↑i)
haveI := hne.to_subtype
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.100664
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (range fun x => f ↑x)
hne : Set.Nonempty s
this : Nonempty ↑s
⊢ l (⨆ (i : ↑s), f ↑i) = ⨆ (i : ↑s), l (f ↑i)
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.100664
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : Set.Nonempty s
this : Nonempty ↑s
⊢ l (⨆ (i : ↑s), f ↑i) = ⨆ (i : ↑s), l (f ↑i)
rw [image_eq_range] at hf
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.100664
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (range fun x => f ↑x)
hne : Set.Nonempty s
this : Nonempty ↑s
⊢ l (⨆ (i : ↑s), f ↑i) = ⨆ (i : ↑s), l (f ↑i)
exact gc.l_ciSup hf