rw [sup_attach]
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) = sup (attach (filter (fun a => p a) univ)) fun x => f ↑x
no goals