Indexed union in complete lattice

Stream: Is there code for X?

[Michael Rothgang]

This one comes from a lemma in sphere-eversion that I'd like to generalise and upstream. This is the statement I would like to prove.

theorem iSup_le {β ι : Type*} [PartialOrder ι] [CompleteLattice β] (s : ι → β) (i : ι) :
    (⨆ j ≤ i, s j) = (⨆ j < i, s j) ⊔ s i := by
  simp only [le_iff_lt_or_eq]
  sorry

Here's the corresponding version for sets.

theorem bUnion_le {α ι : Type*} [PartialOrder ι] (s : ι → Set α) (i : ι) :
    (⋃ j ≤ i, s j) = (⋃ j < i, s j) ∪ s i := by
  simp only [le_iff_lt_or_eq]
  erw [biUnion_union, biUnion_singleton]
  rfl

There might well exist analogues of biUnion_{union,singleton} for complete lattices: I'm not even sure how to state them (the obvious thing I tried failed), so help with that would also be welcome!

[Jireh Loreaux]

It's this not docs#biSup_sup ?

[Jireh Loreaux]

(or a variation on it)

[Jireh Loreaux]

There's also docs#iSup_insert and some Nat-specific lemmas which are closely related.

[Yury G. Kudryashov]

See also docs#iSup_or

[Yaël Dillies]

Yes we don't want one lemma for each specialised Or. Please use iSup_or