Library Coqtail.Reals.Ranalysis.Rfunction_def

Require Import Reals.

Open Scope Rfun_scope.

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.