English
For any f: Nat→(α→ℝ≥0∞), m: Nat, a∈α, the supremum over k≤m+1 of f k a equals the maximum of f (m+1) a and the supremum over k≤m of f k a.
Русский
Для произвольной f: Nat→(α→ℝ≥0∞) и натурального m, a∈α равенство интегративных верхних граней: sup_{k≤m+1} f k a = max{ f(m+1, a), sup_{k≤m} f k a }.
LaTeX
$$$$ \\bigvee_{k \\le m+1} f_k(a) = f_{m+1}(a) \\vee \\bigg( \\bigvee_{k \\le m} f_k(a) \\bigg). $$$$
Lean4
theorem iSup_succ_eq_sup {α} (f : ℕ → α → ℝ≥0∞) (m : ℕ) (a : α) :
⨆ (k : ℕ) (_ : k ≤ m + 1), f k a = f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a :=
by
set c := ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a with hc
set d := f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a with hd
rw [le_antisymm_iff, hc, hd]
constructor
· refine iSup₂_le fun n hn ↦ ?_
rcases Nat.of_le_succ hn with (h | h)
· exact le_sup_of_le_right (le_iSup₂ (f := fun k (_ : k ≤ m) ↦ f k a) n h)
· exact h ▸ le_sup_left
· refine sup_le ?_ (biSup_mono fun n hn ↦ hn.trans m.le_succ)
exact @le_iSup₂ ℝ≥0∞ ℕ (fun i ↦ i ≤ m + 1) _ _ (m + 1) le_rfl
