From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 28 May 2012 11:42:02 +0000 (+0000)
Subject: graph of a function
X-Git-Tag: make_still_working~1686
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a15a68bdd7d5337f2d6f7573dbdb651c5d278cc4;p=helm.git

graph of a function
---

diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma
index babbf997c..d72388dfb 100644
--- a/matita/matita/lib/basics/finset.ma
+++ b/matita/matita/lib/basics/finset.ma
@@ -233,3 +233,26 @@ unification hint  0 ≔ C1,C2;
 (* ---------------------------------------- *) ⊢ 
     T1×T2 ≡ FinSetcarr X.
 
+(* graph of a function *)
+
+definition graph_of ≝ λA,B.λf:A→B. 
+  Σp:A×B.f (\fst p) = \snd p.
+
+definition graph_enum ≝ λA,B:FinSet.λf:A→B. 
+  filter ? (λp.f (\fst p) == \snd p) (enum (FinProd A B)).
+  
+lemma graph_enum_unique : ∀A,B,f.
+  uniqueb ? (graph_enum A B f) = true.
+#A #B #f @uniqueb_filter @(enum_unique (FinProd A B))
+qed.
+
+lemma graph_enum_correct: ∀A,B:FinSet.∀f:A→B. ∀a,b.
+memb ? 〈a,b〉 (graph_enum A B f) = true → f a = b.
+#A #B #f #a #b #membp @(\P ?) @(filter_true … membp)
+qed.
+
+lemma graph_enum_complete: ∀A,B:FinSet.∀f:A→B. ∀a,b.
+f a = b → memb ? 〈a,b〉 (graph_enum A B f) = true.
+#A #B #f #a #b #eqf @memb_filter_l [@(\b eqf)]
+@enum_prod_complete //
+qed.