Documentation

Lean 4 Proof

private theorem simplex_component_le_one {J : ℕ} {p : Fin J → ℝ}
    (hp : OnOpenSimplex J p) (j : Fin J) : p j ≤ 1 := by
  have : p j ≤ ∑ i : Fin J, p i :=
    Finset.single_le_sum (fun i _ => le_of_lt (hp.1 i)) (Finset.mem_univ j)
  linarith [hp.2]

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/Welfare.lean:21

Module Section

Theorem 8, Corollary 6, Propositions 18-22:

In the same file