Documentation

Lean 4 Proof

theorem OnOpenSimplex.toSimplex {p : Fin J → ℝ} (hp : OnOpenSimplex J p) :
    OnSimplex J p :=
  ⟨fun j => le_of_lt (hp.1 j), hp.2⟩

Dependency Graph

Location

thesis/CESProofs/Potential/Defs.lean:212

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file