Axiom functional_extensionality_dep : forall {A : Type} {B : A -> Type} (f g : forall x : A, B x),
(forall x : A, f x = g x) -> f = g.
Lemma functional_extensionality {A B} (f g : A -> B) :
(forall x, f x = g x) -> f = g. Proof. intros ; eauto using @functional_extensionality_dep. Qed.
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.
