Preferred spelling of Sup (e '' s)

Stream: mathlib4

[Violeta Hernández]

The lemma docs#OrderIso.map_sSup is spelled with ⨆ x : s, e x, while docs#OrderIso.map_sSup' uses Sup (e '' s). What's the preferred form?

[Violeta Hernández]

I want to prove some lemmas that are analogous to this but I don't want to be adding any new primed lemmas.

[Eric Wieser]

@Kevin Buzzard and I were discussing this recently; my vote was that you should keep sSup on the RHS if it was present on the LHS, but I think @Yury G. Kudryashov argues we should always use iSup on the RHS if we can

[Violeta Hernández]

My own two cents is that I find it very awkward to write ⨆ x : s. I could understand ⨆ x ∈ s but that's subject to the binder weirdness that's been previously discussed.

[Yury G. Kudryashov]

I agree that we should use sSup (e '' s) for conditionally complete lattices. I would use ⨆ x ∈ s, e x for complete lattices.

[Yury G. Kudryashov]

(or disable this notation)

[Eric Wieser]

Would you also argue for using ⨆ x ∈ s, x in complete lattices instead of sSup s?

[Yury G. Kudryashov]

No.

[Eric Wieser]

Ah, that's unfortunate. I was hoping we could declare it the simp-normal form there, and then we could have our lemmas as:

1. sSup s = ⨆ x ∈ s, x as a simp lemma
2. f (⨆ i, x i) = ⨆ i, f (x i) for people working with the simp-normal form
3. f (sSup s) = sSup (f '' s) for people who know that in their application sSup really is easier
4. No f (sSup s) = ⨆ i, f (x i) lemmas at all, if you want these you have to go through lemma 1

[Yury G. Kudryashov]

More precisely: I'm equally happy with sSup s and ⨆ x ∈ s, x. It would be nice not to have simp normal form so much dependent on α being a conditionally complete lattice or a complete lattice.

[Yury G. Kudryashov]

(I have no proposals)

[Eric Wieser]

Would you be opposed to a refactor doing 2, 3, and 4, but leaving 1 as not simp to avoid that simp-normal form weirdness?

[Eric Wieser]

That is, to switch between sSup and iSup you have to ask explicitly, and otherwise all the lemmas only exist in one world or the other.

[Violeta Hernández]

I like the idea of keeping sSup and iSup separate

[Violeta Hernández]

That way we don't have to write our lemmas in every single combination of sSup and iSup

[Violeta Hernández]

I do think ⨆ x ∈ s, x is a very silly spelling. If we're going to be using this, why have sSup at all?

[Yury G. Kudryashov]

I wouldn't oppose such a refactor.

[Violeta Hernández]

Well, for the moment being, I would like some sort of consensus on how to write these map_xSup lemmas.

[Violeta Hernández]

Should I apply the 2, 3, 4 refactor to at least this subset of results?