converge

Stream: new members

[tsuki hao]

Is there an operation to take a column of elements and converge to one element in lean?

[Jireh Loreaux]

What does a column of elements mean? Can you provide a #mwe?

[tsuki hao]

Jireh Loreaux said:

What does a column of elements mean? Can you provide a #mwe?

This occurs during a proof： Take the element xk → x_bar of the α-lower level set, notice that (xk,α) ∈ epi f and(xk,α) → (x_bar,α), since epi f is a closed set, we know that (x_bar,α) ∈ epi f, that is, f(x_bar) ⩽ α. This explains any α-lower level set of f(x) is closed

[Kevin Buzzard]

Can you provide a #mwe ?