OAI/Geometry/TamingCompatibility/DifferentialForms/ClosedUnitEvaluation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.metric_normalize line 25
2. instance OAI.TamingCompatibility.(instance at line 35) line 35
3. lemma OAI.TamingCompatibility.tames_iff_unitEvaluation_pos line 42
4. def OAI.TamingCompatibility.closedUnitEvaluation line 64