Documentation

Lean 4 Proof

theorem shareFunction_nonneg {w : Fin J → ℝ}
    (hw : ∀ j, 0 ≤ w j) (j : Fin J) :
    0 ≤ shareFunction w j :=
  div_nonneg (hw j) (Finset.sum_nonneg fun k _ => hw k)

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:74

Module Section

Ten Views of a Single Object:

In the same file