proposition: Lemma map2_continuous' `{!Rounded A} `{!Rounded B} `{!Continuous f} `{!Continuous g} : Continuous (map2 f g).
proof: Proof. intros u e. apply (merely_destruct (continuous f (fst u) e));intros [d1 E1]. apply (merely_destruct (continuous g (snd u) e));intros [d2 E2]. apply tr;exists (meet d1 d2). intros v xi. split;simpl. - apply E1. apply rounded_le with (meet d1 d2). + apply xi. + apply meet_lb_l. - apply E2. apply rounded_le with (meet d1 d2). + apply xi. + apply meet_lb_r. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.rationals HoTT.Classes.interfaces.orders HoTT.Classes.implementations.peano_naturals HoTT.Classes.implementations.natpair_integers HoTT.Classes.theory.groups HoTT.Classes.theory.integers HoTT.Classes.theory.dec_fields HoTT.Classes.orders.dec_fields HoTT.Classes.orders.sum HoTT.Classes.theory.rationals HoTT.Classes.orders.lattices HoTT.Classes.implementations.assume_rationals HoTT.Classes.tactics.ring_quote HoTT.Classes.tactics.ring_tac