OAI/Geometry/TamingCompatibility/Currents/LocalMeasure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.LocalRestriction.localMeasure line 13
2. def OAI.TamingCompatibility.LocalRestriction.restrict line 15
3. lemma OAI.TamingCompatibility.LocalRestriction.restrict_coe line 21
4. lemma OAI.TamingCompatibility.LocalRestriction.restrict_norm_le line 28
5. lemma OAI.TamingCompatibility.LocalRestriction.restrict_opNorm_le line 41
6. lemma OAI.TamingCompatibility.LocalRestriction.finite_localMeasure line 47