Lub of finset

Stream: new members

[Jason KY.]

I am trying to create a bounded continuous function as the maximum of finitely many other bounded continuous functions.
I created a lub for this purpose but I have no idea how to join them together using something like \Lub.
Does something like this exist in the library?

import topology.bounded_continuous_function

noncomputable theory
open set

variables {X : Type*} [metric_space X] [compact_space X]

theorem max_bounded {f g : X → ℝ}
(hf :  ∃ (C : ℝ), ∀ (x y : X), dist (f x) (f y) ≤ C)
(hg :  ∃ (C : ℝ), ∀ (x y : X), dist (g x) (g y) ≤ C) :
∃ (C : ℝ), ∀ (x y : X), dist (max (f x) (g x)) (max (f y) (g y)) ≤ C := sorry

instance : has_sup (bounded_continuous_function X ℝ) :=
⟨λ f g, ⟨λ x, max (f x) (g x), continuous.max f.2.1 g.2.1, max_bounded f.2.2 g.2.2⟩⟩

variables {I : finset X} {f : X → bounded_continuous_function X ℝ}

def h : bounded_continuous_function X ℝ := ⨆(i ∈ I), f i
-- It seems to me that `\Lub` is binded to `has_Sup` so I probably can't use that.

[Reid Barton]

I think you want finset.sup.