List.maximum _ < List.minimum

Stream: Is there code for X?

[Jakob von Raumer]

What's the correct type to do this in? Something that both WithTop _ and WithBot _ coerce into, with the obvious inherited order?

[Yaël Dillies]

Typo? :grinning:

[Eric Wieser]

I would expect [1, 2].maximum > [1, 2].minimum but [].maximum < [].minimum

[Jakob von Raumer]

Ah no, no Typo. Was thinking of [1, 2].maximum < [3, 4].minimum.

[Yaël Dillies]

Should we instead have List.max? : List α → WithTop α and List.max : List α → α?

[Jakob von Raumer]

Eric Wieser said:

I would expect [1, 2].maximum > [1, 2].minimum but [].maximum < [].minimum

Exactly. Right now, I can write down the inequality but Lean interprets it as in WithBot Nat because it adapts the type of the RHS and WithBot Nat === Option Nat == WithTop Nat.

[Jakob von Raumer]

While the correct type would be the order isomorphic to WithBot (WithTop Nat) or WithTop (WithBot Nat).

[Eric Wieser]

example : ([1, 2].maximum).map WithTop.some > WithBot.some ([1, 2].minimum) := sorry

works

[Eric Wieser]

I think it might make sense to add a WithTopBot X as an abbreviation or synonym for WithTop (WithBot X), with suitable coercions

[Jakob von Raumer]

Was wondering if there's a more canonical name for that completion

[Kevin Buzzard]

docs#Order.krullDim takes values in Nat with a top and bottom element, and they seem to use WithBot ℕ∞

[Ruben Van de Velde]

There's also EReal