OAI/Combinatorics/BinaryEdit/WordFinite.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.TreeEdit.BinaryLower.wordFinite line 14

   Source documentation

   Exact-length words form a finite type over every finite alphabet.

   instance wordFinite [Finite α] (n : ℕ) : Finite (Word α n) :=
   …

   Mentions: OAI.TreeEdit.Word

2. instance OAI.TreeEdit.BinaryLower.wordsLEFinite line 19

   Source documentation

   At-most-length words form a finite type; the length is retained as a finite sigma index, so repetitions and the empty word are included.

   instance wordsLEFinite [Finite α] (d : ℕ) : Finite (WordsLE α d) := by
   …

   Mentions: OAI.TreeEdit.BinaryLower.WordsLE

3. instance OAI.TreeEdit.BinaryLower.wordsLEInhabited line 28

   Source documentation

   The empty word is included even at cap zero.

   instance wordsLEInhabited (d : ℕ) : Inhabited (WordsLE α d) :=
   …

   Mentions: OAI.TreeEdit.BinaryLower.WordsLE

4. theorem OAI.TreeEdit.BinaryLower.wordsLE_nontrivial line 32

   Source documentation

   A positive cap and a nonempty alphabet already give two distinct words.

   theorem wordsLE_nontrivial [Nonempty α] {d : ℕ} (hd : 1 ≤ d) :
       Nontrivial (WordsLE α d) := by
   …

   Mentions: OAI.TreeEdit.BinaryLower.WordsLE