OAI/Geometry/Convex/GeneralMahler/SimplexCone.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

§§01,06: Full-dimensional simplicial cones and simplex sections.

  1. def OAI.GeneralMahler.IsSimplex line 14

    Source documentation

    Exact affine simplex family.

    def IsSimplex (K : Set (Rn n)) : Prop :=
…

    Mentions: OAI.GeneralMahler.Rn

  2. theorem OAI.GeneralMahler.lift_finrank line 17
  3. def OAI.GeneralMahler.hgtL line 22

    Source comment

    two projection maps for finite linear combinations
    def hgtL : LiftSpace n →ₗ[ℝ] ℝ where
…

    Mentions: OAI.GeneralMahler.LiftSpace

  4. def OAI.GeneralMahler.horizL line 26
  5. theorem OAI.GeneralMahler.hgtL_apply line 30
  6. theorem OAI.GeneralMahler.horizL_apply line 31
  7. lemma OAI.GeneralMahler.independence_lift line 33
  8. theorem OAI.GeneralMahler.sum_coords line 59
  9. lemma OAI.GeneralMahler.Body.exists_basis_of_simplex line 65
  10. theorem OAI.GeneralMahler.Body.simplex_of_linearOrthant line 110