OAI/Geometry/TranslativeCovering/SourceLocalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SourceLocalization.Space line 65
2. abbrev OAI.SourceLocalization.Patterns line 66
3. lemma OAI.SourceLocalization.good_mono_inner line 67
4. lemma OAI.SourceLocalization.low_le line 71
5. lemma OAI.SourceLocalization.pattern_good line 76
6. lemma OAI.SourceLocalization.localize line 80