*)
(* UNEXPORTED
-Section Intervals.
+Section Intervals
*)
(*#* printing realline %\ensuremath{\RR}% #(-∞,+∞)# *)
(* begin hide *)
-coercion "cic:/matita/CoRN-Decl/ftc/MoreIntervals/iprop.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/ftc/MoreIntervals/iprop.con 0 (* compounds *).
(* end hide *)
inline "cic:/CoRN/ftc/MoreIntervals/iprop_wd.con".
(* UNEXPORTED
-End Intervals.
+End Intervals
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Compact_Constructions.
+Section Compact_Constructions
*)
(* UNEXPORTED
-Section Single_Compact_Interval.
+Section Single_Compact_Interval
*)
(*#* **Constructions with Compact Intervals
%\end{convention}%
*)
-inline "cic:/CoRN/ftc/MoreIntervals/P.var".
+alias id "P" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/P.var".
-inline "cic:/CoRN/ftc/MoreIntervals/wdP.var".
+alias id "wdP" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/wdP.var".
-inline "cic:/CoRN/ftc/MoreIntervals/x.var".
+alias id "x" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/x.var".
-inline "cic:/CoRN/ftc/MoreIntervals/Hx.var".
+alias id "Hx" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/Hx.var".
inline "cic:/CoRN/ftc/MoreIntervals/compact_single.con".
inline "cic:/CoRN/ftc/MoreIntervals/compact_single_inc.con".
(* UNEXPORTED
-End Single_Compact_Interval.
+End Single_Compact_Interval
*)
(*#*
*)
(* UNEXPORTED
-Section Proper_Compact_with_One_or_Two_Points.
+Section Proper_Compact_with_One_or_Two_Points
*)
(* begin hide *)
-inline "cic:/CoRN/ftc/MoreIntervals/cip1'.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
-inline "cic:/CoRN/ftc/MoreIntervals/cip1''.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
-inline "cic:/CoRN/ftc/MoreIntervals/cip1'''.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
-inline "cic:/CoRN/ftc/MoreIntervals/cip1''''.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
-inline "cic:/CoRN/ftc/MoreIntervals/cip2.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
-inline "cic:/CoRN/ftc/MoreIntervals/cip2'.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
-inline "cic:/CoRN/ftc/MoreIntervals/cip2''.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
-inline "cic:/CoRN/ftc/MoreIntervals/cip2'''.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
-inline "cic:/CoRN/ftc/MoreIntervals/cip3.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
-inline "cic:/CoRN/ftc/MoreIntervals/cip3'.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
-inline "cic:/CoRN/ftc/MoreIntervals/cip3''.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
-inline "cic:/CoRN/ftc/MoreIntervals/cip3'''.con".
+inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__".
(* end hide *)
inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_rht.con".
(* UNEXPORTED
-End Proper_Compact_with_One_or_Two_Points.
+End Proper_Compact_with_One_or_Two_Points
*)
(*#*
inline "cic:/CoRN/ftc/MoreIntervals/compact_proper_in_interval.con".
(* UNEXPORTED
-End Compact_Constructions.
+End Compact_Constructions
*)
(* UNEXPORTED
-Section Functions.
+Section Functions
*)
(*#* **Properties of Functions in Intervals
%\end{convention}%
*)
-inline "cic:/CoRN/ftc/MoreIntervals/n.var".
+alias id "n" = "cic:/CoRN/ftc/MoreIntervals/Functions/n.var".
-inline "cic:/CoRN/ftc/MoreIntervals/I.var".
+alias id "I" = "cic:/CoRN/ftc/MoreIntervals/Functions/I.var".
inline "cic:/CoRN/ftc/MoreIntervals/Continuous.con".
inline "cic:/CoRN/ftc/MoreIntervals/Diffble_n.con".
(* UNEXPORTED
-End Functions.
+End Functions
*)
(* UNEXPORTED
-Section Reflexivity_Properties.
+Section Reflexivity_Properties
*)
(*#*
inline "cic:/CoRN/ftc/MoreIntervals/Int_Diffble.con".
(* UNEXPORTED
-End Reflexivity_Properties.
+End Reflexivity_Properties
*)
(* UNEXPORTED
-Section Lemmas.
+Section Lemmas
*)
(*#*
inline "cic:/CoRN/ftc/MoreIntervals/included_Feq'.con".
(* UNEXPORTED
-End Lemmas.
+End Lemmas
*)
(* UNEXPORTED