OAI/Geometry/SplitTangent/SymmetricConormalBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Symmetric Conormal Bound.

  1. def OAI.SplitTangent.symmetricSupportedTensors.contractionJet line 26
  2. theorem OAI.SplitTangent.symmetricSupportedTensors.contractionJet_injective line 33
  3. theorem OAI.SplitTangent.symmetricSupportedTensors.finite_and_finrank_le line 63
  4. theorem OAI.SplitTangent.symmetricSupportedTensors.eq_zero_of_degree_lt_order line 79