proposition: Lemma Rmax_continuous : continuous_2arg Rmax (X:=RTop) (Y:=RTop) (Z:=RTop).
proof: Proof. red. replace (fun p : RTop * RTop => _) with (fun p : RTop * RTop => ((fst p) + (snd p) + Rabs (fst p - snd p))*(1/2)). 2: { apply functional_extensionality. intros []. simpl. symmetry. apply Rmax_using_Rabs. } apply @continuous_composition_2arg with (X := RTop) (Y := RTop). 2: { apply continuous_constant. } 2: { apply Rmult_continuous. } apply @continuous_composition_2arg with (X := RTop) (Y := RTop). 3: { apply Rplus_continuous. } - apply @continuous_composition_2arg with (X := RTop) (Y := RTop). + apply product2_fst_continuous. + apply product2_snd_continuous. + apply Rplus_continuous. - apply @continuous_composition with (Y := RTop). { apply Rabs_continuous. } apply @continuous_composition_2arg with (X := RTop) (Y := RTop). + apply product2_fst_continuous. + apply product2_snd_continuous. + apply Rminus_continuous. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)