Defining maximum of prefix of a sequence

Stream: new members

[Nir Paz]

I want to define the maximum of the first n elements of a sequence:

def max_prefix (s : ℕ → ℕ) (n : ℕ) : ℕ := by sorry

I thought about doing this by defining a List of the first n numbers, but I couldn't find a simple way to do this.

[Kevin Buzzard]

What do you want to happen when n=0?

[Nir Paz]

Doesn't really matter, let's say it's 0

[Yaël Dillies]

docs#partialSups

[Nir Paz]

Yaël Dillies said:

docs#partialSups

Thanks! I guess my library searching skills need some improvement

[Yaël Dillies]

Don't worry. It's really not obvious knowing your way around the library! Here you may have been able to guess the name by the fact that your operation is taking max of s (n + 1) with max_prefix s n. But then there's no need for it to be a max for that to be well-defined, so replace it with ⊔ (sup). Probably the name contains "sup". Then it's guesswork to find that it will have "partial" in the name.