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 e9d4ea3 commit 50692cbCopy full SHA for 50692cb
LeanCamCombi/ProbLYM.lean
@@ -57,7 +57,7 @@ theorem card_numberingOn (s : Finset α) : card (NumberingOn s) = s.card.factori
57
58
/-- `IsPrefix s f` means that the elements of `s` precede the elements of `sᶜ`
59
in the numbering `f`. -/
60
-def IsPrefix (s : Finset α) (f : Numbering α) :=
+def Numbering IsPrefix (s : Finset α) (f : Numbering α) :=
61
∀ x, x ∈ s ↔ f x < s.card
62
63
omit [DecidableEq α] in
0 commit comments