criterion for equality in WithTop

Stream: Is there code for X?

[David Loeffler]

The following API lemma – characterizing an element of WithTop M by which elements of M are ≤ to it – would be helpful to have. Do we already have it under some other name? I didn't find it with a search.

variable {M : Type*} [PartialOrder M] [NoMaxOrder M]

lemma eq_of_forall_coe_le_iff {m m' : WithTop M} (hm : ∀ n : M, n ≤ m ↔ n ≤ m') : m = m' := sorry

[David Loeffler]

I made #24165 for this (I can always close the PR if it turns out the functionality already exists)

[Aaron Liu]

Is there a reason why we can't have this in an arbitrary partial order?

[Aaron Liu]

Is this is just docs#eq_of_forall_le_iff (it's not, since you're quantifying over M instead of WithTop M)

[David Loeffler]

No, this is not eq_of_forall_le_iff because n varies over M, not over WithTop M.

[Yaël Dillies]

No we're missing this, thanks for spotting! PR reviewed

[Eric Wieser]

Presumably there could be a version with IsMax?

[David Loeffler]

Not sure what you’re after there. WithTop for orders that already have a max element is not well behaved (the old and new top elements are order-indistinguishable) and it’s not clear why it would be useful anyway.

[Eric Wieser]

I mean for IsMax instead of WithTop

[David Loeffler]

But then it’s just docs#eq_of_forall_le_iff.

[Eric Wieser]

I was imagining that with an extra condition that c is not top

[Eric Wieser]

But either way the version you asked for is worth having