Proof the picewise-linear function is Continuous

Stream: new members

[Junjie Bai]

I want to proof a picewise-linear function is Continuous on R, it's linear function in every section [n, n + 1), n \in N, which function should i use?

[Daniel Weber]

Do you have a #mwe? How do you represent a piecewise-linear function?

[Junjie Bai]

I have represent a piecewis-linear function, it's like :

def piecewiselinear (u : ℝ) : ∑ x in Finset.Icc 1 (⌈u⌉ - 1), (g x) + (u - ⌈u⌉ + 1) * (g ⌈u⌉) := by sorry

where g is a sequence indexed in Z, g i is always less than 1 and great than 0, and when u is less than 0, its always id function.

[Ruben Van de Velde]

Please read #mwe

[Ruben Van de Velde]

(that's a link)