iSup syntax

Stream: new members

[VayusElytra]

Hi, I've been working with iSup quite a bit lately and there is some aspect of its syntax that confuses me.
Let's say we have the following variables:

variable (ι α κ : Type*) [CompleteLattice κ] [CompleteLattice α] (f : ι → κ → α) (k : κ) (i : ι)

1) What is (⨆ j, ⨆ (_ : ¬j = i), f j k) exactly? (i think I understand this but it can't hurt to ask)

2) In this setting I can consider both (⨆ j, ⨆ (_ : ¬j = i), f j k) and (⨆ j, ⨆ (_ : j ≠ i), f j) k). How do they differ exactly? I understand that they are not the same thing to Lean, and that there is a theorem that turns one into the other (iSup_apply) but I'd like to understand what they are. My hunch is that the first takes a sup over the f j k, which are elements in α, and the latter takes a sup over functions κ → α, then applies it at k - and those things happen to be equal because we're implicitly working with a nice enough lattice structure on functions κ → α. Is that it?

3) The file for the theory of complete lattices uses iSup₂ and biiSup to refer to doubles supremums. How are they defined exactly and how do they differ from each other?

Thank you very much for your help :)

[Daniel Weber]

docs#iSup_apply

[Ruben Van de Velde]

2 sounds correct

[Daniel Weber]

Regarding (2), I believe Sup of functions is simply defined pointwise, so they are equal

[Daniel Weber]

In (1) you have a supremum over all j of the supremum over all proofs of i ≠ j of f j k. When j = i that will be the supremum of an empty type, which will be the bottom element, otherwise you have a constant function whose supremum is f j k

[Daniel Weber]

In (3) from what I'm seeing it's just terminology for an iSup inside an iSup

[Yaël Dillies]

Daniel Weber said:

In (3) from what I'm seeing it's just terminology for an iSup inside an iSup

Not quite. An iSup inside an iSup is iSup₂. The special case of an iSup indexed by a Prop inside an iSup is called biSup. This is all explained in the docstring

[Yaël Dillies]

This special case is important due to things like monotonicity in the Prop, attainment of the sup when the inner Prop only has finitely many true values, etc... all things which don't make sense for a general iSup₂

[VayusElytra]

so sorry - i forgot to say thank you all! that was very helpful :)