Zulip Chat Archive

Stream: new members

Topic: Lub of finset

view this post on Zulip Jason KY. (May 28 2020 at 17:00):

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.

view this post on Zulip Reid Barton (May 28 2020 at 17:04):

I think you want finset.sup.

Last updated: May 18 2021 at 16:25 UTC