OAI/Analysis/FreeWords/PatchingWordFamilies.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.KKLocalPatching.PatchingWord.Admissibleline 16 - theorem
OAI.KKLocalPatching.PatchingWord.admissible_finiteline 20 - theorem
OAI.KKLocalPatching.PatchingWord.norm_value_le_oneline 52