OAI/Geometry/Convex/GeneralMahler/Brouwer/Simplex.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Brouwer fixed point for the standard simplex.

  1. abbrev OAI.GeneralMahler.simplexSet line 10

    Source documentation

    Nonnegative weights of total mass one in the ambient function space.

    abbrev simplexSet (I : Type*) [Fintype I] : Set (I → ℝ) :=
…
  2. lemma OAI.GeneralMahler.lattice_approx line 15
  3. theorem OAI.GeneralMahler.BrouwerSimplex line 61