Correctness of continuous functions.
We show that if two functions, one on IR and one on CR, agree on the rational values of some closed interval, and both functions are continuous, then the two functions agree on that entire closed interval.This is our main method of proving the corrections of functions defined on CR.
Lemma Q_dense_in_compact : forall a b (Hab : a[<=]b) x, a[<]b -> Compact Hab x ->
forall e, 0[<]e -> {q:Q | Compact Hab (inj_Q IR q) | AbsSmall e (x[-]inj_Q IR q)}.
Section ContinuousCorrect.
Variable I : interval.
Hypothesis HI : proper I.
Variable f : PartFunct IR.
Hypothesis Hf : Continuous I f.
Variable g : CR --> CR.
Hypothesis Hg : forall (q:Q) Hq, I (inj_Q IR q) -> (g (' q) == IRasCR (f (inj_Q IR q) Hq))%CR.
Lemma ContinuousCorrect : forall (x:IR) Hx, I x -> (IRasCR (f x Hx) == g (IRasCR x))%CR.
End ContinuousCorrect.
forall e, 0[<]e -> {q:Q | Compact Hab (inj_Q IR q) | AbsSmall e (x[-]inj_Q IR q)}.
Section ContinuousCorrect.
Variable I : interval.
Hypothesis HI : proper I.
Variable f : PartFunct IR.
Hypothesis Hf : Continuous I f.
Variable g : CR --> CR.
Hypothesis Hg : forall (q:Q) Hq, I (inj_Q IR q) -> (g (' q) == IRasCR (f (inj_Q IR q) Hq))%CR.
Lemma ContinuousCorrect : forall (x:IR) Hx, I x -> (IRasCR (f x Hx) == g (IRasCR x))%CR.
End ContinuousCorrect.