fold_max_add — Mathlib

English

Folding with max and addition distributes over the Finset elements as shown by the equality.

Русский

Сведение через max и прибавление распределяется по элементам множества Finset согласно равенству.

LaTeX

$$$\text{Finset.fold max ⊥ (fun i \mapsto \uparrow(f(i)) + a) s} = \text{Finset.fold max ⊥ (\uparrow \circ f) s} + a$$$

Lean4

theorem fold_max_add [LinearOrder M] [Add M] [AddRightMono M] (s : Finset ι) (a : WithBot M) (f : ι → M) :
    s.fold max ⊥ (fun i ↦ ↑(f i) + a) = s.fold max ⊥ ((↑) ∘ f) + a := by
  classical induction s using Finset.induction_on <;> simp [*, max_add_add_right]

Похожие утверждения