Finset Suprema Helpers

This file collects small lemmas about Finset.sup' that are useful in RL proofs.

We keep these helpers in their own module so RL proof files (finite MDPs, stochastic MDPs, etc.) do not each re-prove the same sup'-algebra facts locally.

References:

• Puterman, Markov Decision Processes (1994), discounted dynamic programming chapter (the “sup is Lipschitz” step in Bellman optimality contraction proofs).
• Bertsekas, Dynamic Programming and Optimal Control, Vol. 1 (contraction/monotonicity arguments).
• mathlib docs for the underlying finset order-theory API: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finset/Lattice/Fold.html

theorem Proofs.RL.sup'_le_add_const {ι : Type} (s : Finset ι) (hs : s.Nonempty) (f g : ι → ℝ) (c : ℝ) (hfg : ∀ i ∈ s, f i ≤ g i + c) : s.sup' hs f ≤ s.sup' hs g + c

If f i ≤ g i + c for all i ∈ s, then sup f ≤ sup g + c over the same nonempty finset.