FormalConjecturesForMathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 1 file
  1. lemma Affine.Simplex.closedInterior_nonempty line 26 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Ring, AddCommGroup, Module, AddTorsor, PartialOrder, ZeroLEOneClass, Nat, Affine.Simplex, Set.Nonempty, Affine.Simplex.closedInterior

    Proof uses: Exists.intro, Membership.mem, Set, Affine.Simplex.points, OfNat.ofNat, Fin, HAdd.hAdd, Affine.Simplex.point_mem_closedInterior

    27 instances, coercions and auxiliary constants left out.