seq_pigeon[T: TYPE, (IMPORTING finite_sets@finite_sets_below,
finite_sets@finite_sets_card_eq)
S: finite_set[T]]: THEORY
BEGIN
w: VAR finseq[(S)]
seq_pigeon_lem: LEMMA
(FORALL (i,j: below(length(w))): i /= j IMPLIES w(i) /= w(j)) IMPLIES
length(w) <= card(S)
seq_pigeon_hole: THEOREM length(w) > card(S) IMPLIES
(EXISTS (i,j: below(length(w))): i /= j AND w(i) = w(j))
END seq_pigeon
[ zur Elbe Produktseite wechseln0.40Quellennavigators
Analyse erneut starten
]
|