Mathlib.Topology.Order.PartialSups._auxLemma.2

theorem Mathlib.Topology.Order.PartialSups._auxLemma.2 : ∀ {ι : Type u_2} {π : ι → Type u_3} [inst : (i : ι) → SemilatticeSup (π i)] (f : ℕ → (i : ι) → π i) (n : ℕ) (i : ι), (partialSups fun x => f x i) n = (partialSups f) n i

The theorem, `Mathlib.Topology.Order.PartialSups._auxLemma.2`, states that for any type `ι`, any function `π` from `ι` to another type, and any function `f` from natural numbers to `π i` (where `i` is an instance of `ι`), the value of the partial supremum of `f` at index `n` for any given `i` is equal to the value at index `n` of the partial supremum of `f` for the same `i`. In other words, the partial supremum function commutes with the function `f`.

More concisely: For any type `ι`, function `π` from `ι` to another type, and function `f` from natural numbers to `π i`, the partial supremum of `f` at index `n` is equal to the value of the partial supremum of `f` at index `n` for the same `i`.