a list of functions

Stream: new members

[tsuki hao]

Does anyone know how to define a family of functions f_alpha and the supremum of this family of functions?

[Pedro Sánchez Terraf]

Tip: You can use double dollar $$f_\alpha$$ for LaTeX: $f_\alpha$.

A family of funcions $\{f_r\}_r$ is simply a function f : β→γ→γ' with two arguments, one for the parameter r : β and one for the domain of each $f_r$=f r (if those domains do not depend on r, otherwise you need a dependent product).

For the case of γ and γ' being the reals, the pointwise sup of the family is written fun x => ⨆ (r : β), f r x (or λ x ↦ ⨆ (r : β), f r x).

[Eric Wieser]

I think ⨆ (r : β), f r also works, and the pointwise-ness is free (see docs#iSup_apply)?

[Pedro Sánchez Terraf]

Eric Wieser said:

I think ⨆ (r : β), f r also works, and the pointwise-ness is free (see docs#iSup_apply)?

Though you fell in the same trap as I did, the reals are not "complete" :wink:

[Eric Wieser]

Does that matter here?

[Eric Wieser]

Your code and my code are the same, and I think its fair to assume that the pointwise sup exists given it was asked for!

[Pedro Sánchez Terraf]

Eric Wieser said:

Does that matter here?

I did for me, in the meantime I was writing an example to check everything worked fine, and that thing surprised me. I also wasn't sure everything was entirely analogous between Complete and ConditionallyComplete

[Pedro Sánchez Terraf]

(concerning notation and the like, I mean)