We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent c899b11 commit 06acfa6Copy full SHA for 06acfa6
LeanCamCombi/ProbLYM.lean
@@ -143,7 +143,7 @@ instance (s : Finset α) :
143
DecidablePred fun f ↦ (IsPrefix s f) := by
144
intro f ; exact Classical.propDecidable ((fun f ↦ IsPrefix s f) f)
145
146
-def SetPrefix (s : Finset α) : Finset (Numbering α) :=
+def Prefixes (s : Finset α) : Finset (Numbering α) :=
147
{f | IsPrefix s f}
148
149
theorem set_prefix_card (s : Finset α) :
0 commit comments