case h
α : Type ?u.63285
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LinearOrder γ
inst✝ : OrderClosedTopology γ
ι : Type u_1
s : Finset ι
H : Finset.Nonempty s
f : ι → C(β, γ)
x✝ : β
⊢ ↑(Finset.sup' s H f) x✝ = Finset.sup' s H (fun a => ↑(f a)) x✝
α : Type ?u.63285
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LinearOrder γ
inst✝ : OrderClosedTopology γ
ι : Type u_1
s : Finset ι
H : Finset.Nonempty s
f : ι → C(β, γ)
⊢ ↑(Finset.sup' s H f) = Finset.sup' s H fun a => ↑(f a)
ext
no goals
case h
α : Type ?u.63285
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LinearOrder γ
inst✝ : OrderClosedTopology γ
ι : Type u_1
s : Finset ι
H : Finset.Nonempty s
f : ι → C(β, γ)
x✝ : β
⊢ ↑(Finset.sup' s H f) x✝ = Finset.sup' s H (fun a => ↑(f a)) x✝
simp [sup'_apply]