variant of sSup_apply with sSup on both sides

Stream: Is there code for X?

[Ira Fesefeldt]

I am looking for something like sSup_apply for the complete Lattice of the pi type but that yields me again an sSup instead of an iSup. So, something like this:

import Mathlib.Data.Real.EReal

def my_type := ℕ → EReal

noncomputable instance : CompleteLattice my_type := Pi.instCompleteLattice

theorem my_sSup_apply {α : Type} {f : α → my_type } {n : ℕ} :
    sSup { x | ∃ y, f y = x} n = sSup { x | ∃ y, f y n = x} := by
  sorry

Is there something like this? I only found sSup_apply, but I don't know how to make this iSup again into an sSup.

[Eric Wieser]

This works:

import Mathlib.Data.Real.EReal

abbrev my_type := ℕ → EReal

theorem my_sSup_apply {α : Type} {f : α → my_type } {n : ℕ} :
    sSup { x | ∃ y, f y = x} n = sSup { x | ∃ y, f y n = x} := by
  rw [sSup_apply, iSup, Set.range]
  simp