|
set_of_functions [ T1, T2: TYPE ]: THEORY
%------------------------------------------------------------------------
% number of functions from finite set A to finite set B
%
% by Bruno Dutertre Royal Holloway & Bedford New College
%
% defines:
%
% funset(A, B): finite_set[[(A)->(B)]] = fullset[[(A)->(B)]]
%
%------------------------------------------------------------------------
BEGIN
IMPORTING fun_below_props,
finite_sets@func_composition
n, m: VAR nat
A: VAR finite_set[T1]
B: VAR finite_set[T2]
empty_finite_domain1 : LEMMA card(A) = 0 IMPLIES
(EXISTS (f: [(A) -> (B)]): TRUE)
empty_finite_domain2 : LEMMA card(A) = 0 IMPLIES
(FORALL (f1, f2: [(A) -> (B)]): f1 = f2)
empty_finite_range : LEMMA card(B) = 0 AND card(A) /= 0 IMPLIES
(FORALL (f: [(A) -> (B)]): FALSE)
finite_funset_bijection1: THEOREM card(A) = n AND card(B) = m IMPLIES
(EXISTS (f: [[(A) -> (B)] -> [below[n] -> below[m]]]): bijective?(f))
finite_funset_bijection2: THEOREM card(A) = n AND card(B) = m IMPLIES
(EXISTS (f: [[(A) -> (B)] -> below[m ^ n]]): bijective?(f))
finite_funset : THEOREM is_finite_type[[(A) -> (B)]]
funset(A, B): finite_set[[(A)->(B)]] = fullset[[(A)->(B)]]
card_funset : THEOREM card(funset(A, B)) = card(B) ^ card(A)
END set_of_functions
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
