# Library Coqtail.Reals.Ranalysis.Rfunction_def

Extensional equality on functions

Definition Rfun_eq (f g : R → R) := ∀ x, f x = g x.

Infix "==" := Rfun_eq (at level 70, no associativity) : Rfun_scope.

Lemma Rfun_eq_refl : ∀ f, f == f.

Proof.

intros f x ; reflexivity.

Qed.

Lemma Rfun_eq_sym : ∀ f g, f == g → g == f.

Proof.

intros f g H x ; auto.

Qed.

Lemma Rfun_eq_trans : ∀ f g h, f == g → g == h → f == h.

Proof.

intros f g h Hfg Hgh ; intro x ; rewrite Hfg, Hgh ; reflexivity.

Qed.

Require Setoid.

Add Parametric Relation : (R → R) Rfun_eq

reflexivity proved by Rfun_eq_refl

symmetry proved by Rfun_eq_sym

transitivity proved by Rfun_eq_trans

as Rf_eq.