notation < "hvbox(Σ ident i opt (: ty) break . p)"
right associative with precedence 20
-for @{ 'exists ${default
+for @{ 'sigma ${default
@{\lambda ${ident i} : $ty. $p)}
@{\lambda ${ident i} . $p}}}.
interpretation "constructive exists" 'sigma \eta.x =
- (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x).
\ No newline at end of file
+ (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x).
apply (inv_inverse_ ? ? (field_properties F)).
qed.
+(*CSC: qua funzionava anche mettendo ? al posto della prima F*)
definition sum_field ≝
- λF:field. sum ? (plus F) 0 1.
+ λF:field. sum F (plus F) 0 1.
set "baseuri" "cic:/matita/integration_algebras/".
include "vector_spaces.ma".
+include "lattices.ma".
-record is_lattice (C:Type) (join,meet:C→C→C) : Prop \def
- { (* abelian semigroup properties *)
- l_comm_j: symmetric ? join;
- l_associative_j: associative ? join;
- l_comm_m: symmetric ? meet;
- l_associative_m: associative ? meet;
- (* other properties *)
- l_adsorb_j_m: ∀f,g. join f (meet f g) = f;
- l_adsorb_m_j: ∀f,g. meet f (join f g) = f
- }.
-
-record lattice (C:Type) : Type \def
- { join: C → C → C;
- meet: C → C → C;
- l_lattice_properties: is_lattice ? join meet
- }.
-
-definition le \def λC:Type.λL:lattice C.λf,g. meet ? L f g = f.
-
-interpretation "Lattice le" 'leq a b =
- (cic:/matita/integration_algebras/le.con _ _ a b).
-
-definition lt \def λC:Type.λL:lattice C.λf,g. le ? L f g ∧ f ≠ g.
-
-interpretation "Lattice lt" 'lt a b =
- (cic:/matita/integration_algebras/lt.con _ _ a b).
-
-definition carrier_of_lattice ≝
- λC:Type.λL:lattice C.C.
+(**************** Riesz Spaces ********************)
record is_riesz_space (K:ordered_field_ch0) (V:vector_space K)
- (L:lattice (Type_OF_vector_space ? V))
+ (L:lattice V)
: Prop
\def
- { rs_compat_le_plus: ∀f,g,h. le ? L f g → le ? L (f+h) (g+h);
- rs_compat_le_times: ∀a:K.∀f. of_le ? 0 a → le ? L 0 f → le ? L 0 (a*f)
+ { rs_compat_le_plus: ∀f,g,h:V. os_le ? L f g → os_le ? L (f+h) (g+h);
+ rs_compat_le_times: ∀a:K.∀f:V. zero K≤a → os_le ? L (zero V) f → os_le ? L (zero V) (a*f)
}.
record riesz_space (K:ordered_field_ch0) : Type \def
rs_riesz_space_properties: is_riesz_space ? rs_vector_space rs_lattice
}.
+record is_positive_linear (K) (V:riesz_space K) (T:V→K) : Prop ≝
+ { positive: ∀u:V. os_le ? V 0 u → os_le ? K 0 (T u);
+ linear1: ∀u,v:V. T (u+v) = T u + T v;
+ linear2: ∀u:V.∀k:K. T (k*u) = k*(T u)
+ }.
+
+record sequentially_order_continuous (K) (V:riesz_space K) (T:V→K) : Prop ≝
+ { soc_incr:
+ ∀a:nat→V.∀l:V.is_increasing ? ? a → is_sup ? V a l →
+ is_increasing ? K (λn.T (a n)) ∧ tends_to ? (λn.T (a n)) (T l)
+ }.
+
definition absolute_value \def λK.λS:riesz_space K.λf.join ? S f (-f).
-(*CSC: qui la notazione non fa capire!!! *)
+(**************** Normed Riesz spaces ****************************)
+
definition is_riesz_norm ≝
- λR:real.λV:riesz_space R.λnorm:norm ? V.
- ∀f,g:V. le ? V (absolute_value ? V f) (absolute_value ? V g) →
- of_le R (norm f) (norm g).
+ λR:real.λV:riesz_space R.λnorm:norm R V.
+ ∀f,g:V. os_le ? V (absolute_value ? V f) (absolute_value ? V g) →
+ os_le ? R (n_function R V norm f) (n_function R V norm g).
record riesz_norm (R:real) (V:riesz_space R) : Type ≝
- { rn_norm:> norm ? V;
+ { rn_norm:> norm R V;
rn_riesz_norm_property: is_riesz_norm ? ? rn_norm
}.
(*CSC: non fa la chiusura delle coercion verso funclass *)
definition rn_function ≝
λR:real.λV:riesz_space R.λnorm:riesz_norm ? V.
- n_function ? ? (rn_norm ? ? norm).
+ n_function R V (rn_norm ? ? norm).
coercion cic:/matita/integration_algebras/rn_function.con 1.
(************************** L-SPACES *************************************)
-
+(*
record is_l_space (R:real) (V:riesz_space R) (norm:riesz_norm ? V) : Prop ≝
{ ls_banach: is_complete ? V (induced_distance ? ? norm);
ls_linear: ∀f,g:V. le ? V 0 f → le ? V 0 g → norm (f+g) = norm f + norm g
}.
-
+*)
(******************** ARCHIMEDEAN RIESZ SPACES ***************************)
record is_archimedean_riesz_space (K) (S:riesz_space K) : Prop
\def
- { ars_archimedean: ∃u.∀n.∀a.∀p:n > O.
- le ? S
+ { ars_archimedean: ∃u:S.∀n.∀a.∀p:n > O.
+ os_le ? S
(absolute_value ? S a)
- ((inv ? (sum_field K n) (not_eq_sum_field_zero ? n p))* u) →
+ ((inv K (sum_field K n) (not_eq_sum_field_zero K n p))* u) →
a = 0
}.
ars_archimedean_property: is_archimedean_riesz_space ? ars_riesz_space
}.
-record is_integral (K) (R:archimedean_riesz_space K) (I:R→K) : Prop
-\def
- { i_positive: ∀f:R. le ? R 0 f → of_le K 0 (I f);
- i_linear1: ∀f,g:R. I (f + g) = I f + I g;
- i_linear2: ∀f:R.∀k:K. I (k*f) = k*(I f)
- }.
-
definition is_weak_unit ≝
(* This definition is by Spitters. He cites Fremlin 353P, but:
1. that theorem holds only in f-algebras (as in Spitters, but we are
irs_unit: irs_archimedean_riesz_space;
irs_weak_unit: is_weak_unit ? ? irs_unit;
integral: irs_archimedean_riesz_space → R;
- irs_integral_properties: is_integral ? ? integral;
+ irs_positive_linear: is_positive_linear ? ? integral;
irs_limit1:
∀f:irs_archimedean_riesz_space.
tends_to ?
definition induced_norm_fun ≝
λR:real.λV:integration_riesz_space R.λf:V.
- integral ? ? (absolute_value ? ? f).
+ integral ? V (absolute_value ? ? f).
lemma induced_norm_is_norm:
- ∀R:real.∀V:integration_riesz_space R.is_norm ? V (induced_norm_fun ? V).
+ ∀R:real.∀V:integration_riesz_space R.is_norm R V (induced_norm_fun ? V).
+ elim daemon.(*
intros;
apply mk_is_norm;
[ apply mk_is_semi_norm;
[ unfold induced_norm_fun;
intros;
- apply i_positive;
- [ apply (irs_integral_properties ? V)
+ apply positive;
+ [ apply (irs_positive_linear ? V)
| (* difficile *)
elim daemon
]
rewrite < eq_zero_opp_zero;
rewrite > zero_neutral;
assumption
- ].
+ ].*)
qed.
definition induced_norm ≝
(* now we prove that any complete integration riesz space is an L-space *)
-theorem is_l_space_l_space_induced_by_integral:
+(*theorem is_l_space_l_space_induced_by_integral:
∀R:real.∀V:complete_integration_riesz_space R.
is_l_space ? ? (induced_riesz_norm ? V).
intros;
(* difficile *)
elim daemon
].
-qed.
+qed.*)
(**************************** f-ALGEBRAS ********************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/lattices/".
+
+include "ordered_sets.ma".
+
+record pre_lattice (C:Type) : Type \def
+ { join_: C → C → C;
+ meet_: C → C → C
+ }.
+
+definition carrier_of_lattice ≝ λC:Type.λL:pre_lattice C.C.
+
+coercion cic:/matita/lattices/carrier_of_lattice.con.
+
+definition join : ∀C.∀L:pre_lattice C.L→L→L ≝ join_.
+definition meet : ∀C.∀L:pre_lattice C.L→L→L ≝ meet_.
+
+interpretation "Lattice meet" 'and a b =
+ (cic:/matita/lattices/meet.con _ _ a b).
+
+interpretation "Lattice join" 'or a b =
+ (cic:/matita/lattices/join.con _ _ a b).
+
+record is_lattice (C:Type) (L:pre_lattice C) : Prop \def
+ { (* abelian semigroup properties *)
+ l_comm_j: symmetric ? (join ? L);
+ l_associative_j: associative ? (join ? L);
+ l_comm_m: symmetric ? (meet ? L);
+ l_associative_m: associative ? (meet ? L);
+ (* other properties *)
+ l_adsorb_j_m: ∀f,g:L. (f ∨ f ∧ g) = f;
+ l_adsorb_m_j: ∀f,g:L. (f ∧ (f ∨ g)) = f
+ }.
+
+record lattice (C:Type) : Type \def
+ { l_pre_lattice:> pre_lattice C;
+ l_lattice_properties:> is_lattice ? l_pre_lattice
+ }.
+
+definition le \def λC:Type.λL:lattice C.λf,g:L. (f ∧ g) = f.
+
+definition ordered_set_of_lattice: ∀C.lattice C → ordered_set C.
+ intros;
+ apply mk_ordered_set;
+ [ apply mk_pre_ordered_set;
+ apply (le ? l)
+ | apply mk_is_order_relation;
+ [ unfold reflexive;
+ intros;
+ unfold;
+ simplify;
+ unfold le;
+ change in x with (carrier_of_lattice ? l);
+ rewrite < (l_adsorb_j_m ? ? l ? x) in ⊢ (? ? (? ? ? ? %) ?);
+ rewrite > l_adsorb_m_j;
+ [ reflexivity
+ | apply (l_lattice_properties ? l)
+ ]
+ | intros;
+ unfold transitive;
+ simplify;
+ unfold le;
+ intros;
+ rewrite < H;
+ rewrite > (l_associative_m ? ? l);
+ rewrite > H1;
+ reflexivity
+ | unfold antisimmetric;
+ unfold os_le;
+ simplify;
+ unfold le;
+ intros;
+ rewrite < H;
+ rewrite > (l_comm_m ? ? l);
+ assumption
+ ]
+ ]
+qed.
+
+coercion cic:/matita/lattices/ordered_set_of_lattice.con.
+
+(*
+interpretation "Lattice le" 'leq a b =
+ (cic:/matita/integration_algebras/le.con _ _ a b).
+
+definition lt \def λC:Type.λL:lattice C.λf,g. le ? L f g ∧ f ≠ g.
+
+interpretation "Lattice lt" 'lt a b =
+ (cic:/matita/integration_algebras/lt.con _ _ a b).
+*)
+
+(* The next coercion introduces a cycle in the coercion graph with
+ unexpected bad results
+coercion cic:/matita/integration_algebras/carrier_of_lattice.con.
+*)
set "baseuri" "cic:/matita/ordered_fields_ch0/".
include "fields.ma".
+include "ordered_sets.ma".
-record is_total_order_relation (C:Type) (le:C→C→Prop) : Type \def
- { to_cotransitive: ∀x,y,z:C. le x y → le x z ∨ le z y;
- to_antisimmetry: ∀x,y:C. le x y → le y x → x=y
- }.
-
-theorem to_transitive:
- ∀C.∀le:C→C→Prop. is_total_order_relation ? le → transitive ? le.
- intros;
- unfold transitive;
- intros;
- elim (to_cotransitive ? ? i ? ? z H);
- [ assumption
- | rewrite < (to_antisimmetry ? ? i ? ? H1 t);
- assumption
- ].
-qed.
-
+(*CSC: non capisco questi alias! Una volta non servivano*)
+alias id "plus" = "cic:/matita/groups/plus.con".
+alias symbol "plus" = "Abelian group plus".
record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Type \def
- { of_total_order_relation:> is_total_order_relation ? le;
- of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
+ { of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
of_plus_compat: ∀a,b,c. le a b → le (a+c) (b+c);
of_weak_tricotomy : ∀a,b. a≠b → le a b ∨ le b a;
(* 0 characteristics *)
- of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0
+ (*CSC: qua c'era un ? al posto di F *)
+ of_char0: ∀n. n > O → sum F (plus F) 0 1 n ≠ 0
}.
record ordered_field_ch0 : Type \def
{ of_field:> field;
- of_le: of_field → of_field → Prop;
- of_ordered_field_properties:> is_ordered_field_ch0 ? of_le
+ of_ordered_set:> ordered_set of_field;
+ of_reflexive: reflexive ? (os_le ? of_ordered_set);
+ of_antisimmetric: antisimmetric ? (os_le ? of_ordered_set);
+ of_cotransitive: cotransitive ? (os_le ? of_ordered_set);
+ (*CSC: qui c'era un ? al posto di of_field *)
+ of_ordered_field_properties:> is_ordered_field_ch0 of_field (os_le ? of_ordered_set)
}.
-interpretation "Ordered field le" 'leq a b =
- (cic:/matita/ordered_fields_ch0/of_le.con _ a b).
-
-definition lt \def λF:ordered_field_ch0.λa,b:F.a ≤ b ∧ a ≠ b.
+(*theorem ordered_set_of_ordered_field_ch0:
+ ∀F:ordered_field_ch0.ordered_set F.
+ intros;
+ apply mk_ordered_set;
+ [ apply (mk_pre_ordered_set ? (of_le F))
+ | apply mk_is_order_relation;
+ [ apply (of_reflexive F)
+ | apply antisimmetric_to_cotransitive_to_transitive;
+ [ apply (of_antisimmetric F)
+ | apply (of_cotransitive F)
+ ]
+ | apply (of_antisimmetric F)
+ ]
+ ].
+qed.
-interpretation "Ordered field lt" 'lt a b =
- (cic:/matita/ordered_fields_ch0/lt.con _ a b).
+coercion cic:/matita/ordered_fields_ch0/ordered_set_of_ordered_field_ch0.con.
+*)
-lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F. 0 ≤ x → -x ≤ 0.
+(*interpretation "Ordered field le" 'leq a b =
+ (cic:/matita/ordered_fields_ch0/of_le.con _ a b).
+ *)
+
+(*CSC: qua c'era uno zero*)
+lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F.(zero F) ≤ x → -x ≤ 0.
intros;
generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
rewrite > zero_neutral in H1;
rewrite > plus_comm in H1;
rewrite > opp_inverse in H1;
- assumption.
+ (*assumption*)apply H1.
qed.
-lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
+(*CSC: qua c'era uno zero*)
+lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → (zero F) ≤ -x.
intros;
generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
rewrite > zero_neutral in H1;
rewrite > plus_comm in H1;
rewrite > opp_inverse in H1;
- assumption.
+ (*assumption.*) apply H1.
qed.
(*
*)
axiom lt_zero_to_lt_inv_zero:
- ∀F:ordered_field_ch0.∀x:F.∀p:x≠0. 0 < x → 0 < inv ? x p.
-
+ ∀F:ordered_field_ch0.∀x:F.∀p:x≠0. lt ? F 0 x → lt ? F 0 (inv ? x p).
+
+alias symbol "lt" = "natural 'less than'".
+
(* The ordering is not necessary. *)
axiom not_eq_sum_field_zero: ∀F:ordered_field_ch0.∀n. O<n → sum_field F n ≠ 0.
-axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → 0 < sum_field F n.
+axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → lt ? F 0 (sum_field F n).
axiom lt_zero_to_le_inv_zero:
- ∀F:ordered_field_ch0.∀n:nat.∀p:sum_field F n ≠ 0. 0 ≤ inv ? (sum_field ? n) p.
+ ∀F:ordered_field_ch0.∀n:nat.∀p:sum_field F n ≠ 0. os_le ? F 0 (inv ? (sum_field ? n) p).
definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
apply
(λF:ordered_field_ch0.λf:nat → F.λl:F.
- ∀n:nat.∃m:nat.∀j:nat. m≤j →
+ ∀n:nat.∃m:nat.∀j:nat. le m j →
l - (inv F (sum_field ? (S n)) ?) ≤ f j ∧
f j ≤ l + (inv F (sum_field ? (S n)) ?));
apply not_eq_sum_field_zero;
apply
(λF:ordered_field_ch0.λf:nat→F.
∀m:nat.
- ∃n:nat.∀N. n ≤ N →
+ ∃n:nat.∀N. le n N →
-(inv ? (sum_field F (S m)) ?) ≤ f N - f n ∧
f N - f n ≤ inv ? (sum_field F (S m)) ?);
apply not_eq_sum_field_zero;
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/ordered_sets/".
+
+include "higher_order_defs/relations.ma".
+include "nat/plus.ma".
+include "constructive_connectives.ma".
+
+record pre_ordered_set (C:Type) : Type ≝
+ { le_:C→C→Prop }.
+
+definition carrier_of_pre_ordered_set ≝ λC:Type.λO:pre_ordered_set C.C.
+
+coercion cic:/matita/ordered_sets/carrier_of_pre_ordered_set.con.
+
+definition os_le: ∀C.∀O:pre_ordered_set C.O → O → Prop ≝ le_.
+
+interpretation "Ordered Sets le" 'leq a b =
+ (cic:/matita/ordered_sets/os_le.con _ _ a b).
+
+definition cotransitive ≝
+ λC:Type.λle:C→C→Prop.∀x,y,z:C. le x y → le x z ∨ le z y.
+
+definition antisimmetric ≝
+ λC:Type.λle:C→C→Prop.∀x,y:C. le x y → le y x → x=y.
+
+record is_order_relation (C) (O:pre_ordered_set C) : Type ≝
+ { or_reflexive: reflexive ? (os_le ? O);
+ or_transitive: transitive ? (os_le ? O);
+ or_antisimmetric: antisimmetric ? (os_le ? O)
+ }.
+
+record ordered_set (C:Type): Type ≝
+ { os_pre_ordered_set:> pre_ordered_set C;
+ os_order_relation_properties:> is_order_relation ? os_pre_ordered_set
+ }.
+
+theorem antisimmetric_to_cotransitive_to_transitive:
+ ∀C.∀le:relation C. antisimmetric ? le → cotransitive ? le →
+ transitive ? le.
+ intros;
+ unfold transitive;
+ intros;
+ elim (c ? ? z H1);
+ [ assumption
+ | rewrite < (H ? ? H2 t);
+ assumption
+ ].
+qed.
+
+definition is_increasing ≝ λC.λO:ordered_set C.λa:nat→O.∀n:nat.a n ≤ a (S n).
+definition is_decreasing ≝ λC.λO:ordered_set C.λa:nat→O.∀n:nat.a (S n) ≤ a n.
+
+definition is_upper_bound ≝ λC.λO:ordered_set C.λa:nat→O.λu:O.∀n:nat.a n ≤ u.
+definition is_lower_bound ≝ λC.λO:ordered_set C.λa:nat→O.λu:O.∀n:nat.u ≤ a n.
+
+record is_sup (C:Type) (O:ordered_set C) (a:nat→O) (u:O) : Prop ≝
+ { sup_upper_bound: is_upper_bound ? O a u;
+ sup_least_upper_bound: ∀v:O. is_upper_bound ? O a v → u≤v
+ }.
+
+record is_inf (C:Type) (O:ordered_set C) (a:nat→O) (u:O) : Prop ≝
+ { inf_lower_bound: is_lower_bound ? O a u;
+ inf_greatest_lower_bound: ∀v:O. is_lower_bound ? O a v → v≤u
+ }.
+
+record is_bounded_below (C:Type) (O:ordered_set C) (a:nat→O) : Type ≝
+ { ib_lower_bound: O;
+ ib_lower_bound_is_lower_bound: is_lower_bound ? ? a ib_lower_bound
+ }.
+
+record is_bounded_above (C:Type) (O:ordered_set C) (a:nat→O) : Type ≝
+ { ib_upper_bound: O;
+ ib_upper_bound_is_upper_bound: is_upper_bound ? ? a ib_upper_bound
+ }.
+
+record is_bounded (C:Type) (O:ordered_set C) (a:nat→O) : Type ≝
+ { ib_bounded_below:> is_bounded_below ? ? a;
+ ib_bounded_above:> is_bounded_above ? ? a
+ }.
+
+record bounded_below_sequence (C:Type) (O:ordered_set C) : Type ≝
+ { bbs_seq:1> nat→O;
+ bbs_is_bounded_below:> is_bounded_below ? ? bbs_seq
+ }.
+
+record bounded_above_sequence (C:Type) (O:ordered_set C) : Type ≝
+ { bas_seq:1> nat→O;
+ bas_is_bounded_above:> is_bounded_above ? ? bas_seq
+ }.
+
+record bounded_sequence (C:Type) (O:ordered_set C) : Type ≝
+ { bs_seq:1> nat → O;
+ bs_is_bounded_below: is_bounded_below ? ? bs_seq;
+ bs_is_bounded_above: is_bounded_above ? ? bs_seq
+ }.
+
+definition bounded_below_sequence_of_bounded_sequence ≝
+ λC.λO:ordered_set C.λb:bounded_sequence ? O.
+ mk_bounded_below_sequence ? ? b (bs_is_bounded_below ? ? b).
+
+coercion cic:/matita/ordered_sets/bounded_below_sequence_of_bounded_sequence.con.
+
+definition bounded_above_sequence_of_bounded_sequence ≝
+ λC.λO:ordered_set C.λb:bounded_sequence ? O.
+ mk_bounded_above_sequence ? ? b (bs_is_bounded_above ? ? b).
+
+coercion cic:/matita/ordered_sets/bounded_above_sequence_of_bounded_sequence.con.
+
+definition lower_bound ≝
+ λC.λO:ordered_set C.λb:bounded_below_sequence ? O.
+ ib_lower_bound ? ? b (bbs_is_bounded_below ? ? b).
+
+lemma lower_bound_is_lower_bound:
+ ∀C.∀O:ordered_set C.∀b:bounded_below_sequence ? O.
+ is_lower_bound ? ? b (lower_bound ? ? b).
+ intros;
+ unfold lower_bound;
+ apply ib_lower_bound_is_lower_bound.
+qed.
+
+definition upper_bound ≝
+ λC.λO:ordered_set C.λb:bounded_above_sequence ? O.
+ ib_upper_bound ? ? b (bas_is_bounded_above ? ? b).
+
+lemma upper_bound_is_upper_bound:
+ ∀C.∀O:ordered_set C.∀b:bounded_above_sequence ? O.
+ is_upper_bound ? ? b (upper_bound ? ? b).
+ intros;
+ unfold upper_bound;
+ apply ib_upper_bound_is_upper_bound.
+qed.
+
+record is_dedekind_sigma_complete (C:Type) (O:ordered_set C) : Type ≝
+ { dsc_inf: ∀a:nat→O.∀m:O. is_lower_bound ? ? a m → ex ? (λs:O.is_inf ? O a s);
+ dsc_inf_proof_irrelevant:
+ ∀a:nat→O.∀m,m':O.∀p:is_lower_bound ? ? a m.∀p':is_lower_bound ? ? a m'.
+ (match dsc_inf a m p with [ ex_intro s _ ⇒ s ]) =
+ (match dsc_inf a m' p' with [ ex_intro s' _ ⇒ s' ]);
+ dsc_sup: ∀a:nat→O.∀m:O. is_upper_bound ? ? a m → ex ? (λs:O.is_sup ? O a s);
+ dsc_sup_proof_irrelevant:
+ ∀a:nat→O.∀m,m':O.∀p:is_upper_bound ? ? a m.∀p':is_upper_bound ? ? a m'.
+ (match dsc_sup a m p with [ ex_intro s _ ⇒ s ]) =
+ (match dsc_sup a m' p' with [ ex_intro s' _ ⇒ s' ])
+ }.
+
+record dedekind_sigma_complete_ordered_set (C:Type) : Type ≝
+ { dscos_ordered_set:> ordered_set C;
+ dscos_dedekind_sigma_complete_properties:>
+ is_dedekind_sigma_complete ? dscos_ordered_set
+ }.
+
+definition inf:
+ ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C.
+ bounded_below_sequence ? O → O.
+ intros;
+ elim
+ (dsc_inf ? O (dscos_dedekind_sigma_complete_properties ? O) b);
+ [ apply a
+ | apply (lower_bound ? ? b)
+ | apply lower_bound_is_lower_bound
+ ]
+qed.
+
+lemma inf_is_inf:
+ ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C.
+ ∀a:bounded_below_sequence ? O.
+ is_inf ? ? a (inf ? ? a).
+ intros;
+ unfold inf;
+ simplify;
+ elim (dsc_inf C O (dscos_dedekind_sigma_complete_properties C O) a
+(lower_bound C O a) (lower_bound_is_lower_bound C O a));
+ simplify;
+ assumption.
+qed.
+
+lemma inf_proof_irrelevant:
+ ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C.
+ ∀a,a':bounded_below_sequence ? O.
+ bbs_seq ? ? a = bbs_seq ? ? a' →
+ inf ? ? a = inf ? ? a'.
+ intros 4;
+ elim a 0;
+ elim a';
+ simplify in H;
+ generalize in match i1;
+ clear i1;
+ rewrite > H;
+ intro;
+ simplify;
+ rewrite < (dsc_inf_proof_irrelevant C O O f (ib_lower_bound ? ? f i2)
+ (ib_lower_bound ? ? f i) (ib_lower_bound_is_lower_bound ? ? f i2)
+ (ib_lower_bound_is_lower_bound ? ? f i));
+ reflexivity.
+qed.
+
+definition sup:
+ ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C.
+ bounded_above_sequence ? O → O.
+ intros;
+ elim
+ (dsc_sup ? O (dscos_dedekind_sigma_complete_properties ? O) b);
+ [ apply a
+ | apply (upper_bound ? ? b)
+ | apply upper_bound_is_upper_bound
+ ].
+qed.
+
+lemma sup_is_sup:
+ ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C.
+ ∀a:bounded_above_sequence ? O.
+ is_sup ? ? a (sup ? ? a).
+ intros;
+ unfold sup;
+ simplify;
+ elim (dsc_sup C O (dscos_dedekind_sigma_complete_properties C O) a
+(upper_bound C O a) (upper_bound_is_upper_bound C O a));
+ simplify;
+ assumption.
+qed.
+
+lemma sup_proof_irrelevant:
+ ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C.
+ ∀a,a':bounded_above_sequence ? O.
+ bas_seq ? ? a = bas_seq ? ? a' →
+ sup ? ? a = sup ? ? a'.
+ intros 4;
+ elim a 0;
+ elim a';
+ simplify in H;
+ generalize in match i1;
+ clear i1;
+ rewrite > H;
+ intro;
+ simplify;
+ rewrite < (dsc_sup_proof_irrelevant C O O f (ib_upper_bound ? ? f i2)
+ (ib_upper_bound ? ? f i) (ib_upper_bound_is_upper_bound ? ? f i2)
+ (ib_upper_bound_is_upper_bound ? ? f i));
+ reflexivity.
+qed.
+
+axiom daemon: False.
+
+theorem inf_le_sup:
+ ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C.
+ ∀a:bounded_sequence ? O. inf ? ? a ≤ sup ? ? a.
+ intros (C O');
+ apply (or_transitive ? ? O' ? (a O));
+ [ elim daemon (*apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? a))*)
+ | elim daemon (*apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? a))*)
+ ].
+qed.
+
+lemma inf_respects_le:
+ ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C.
+ ∀a:bounded_below_sequence ? O.∀m:O.
+ is_upper_bound ? ? a m → inf ? ? a ≤ m.
+ intros (C O');
+ apply (or_transitive ? ? O' ? (sup ? ? (mk_bounded_sequence ? ? a ? ?)));
+ [ apply (bbs_is_bounded_below ? ? a)
+ | apply (mk_is_bounded_above ? ? ? m H)
+ | apply inf_le_sup
+ | apply
+ (sup_least_upper_bound ? ? ? ?
+ (sup_is_sup ? ? (mk_bounded_sequence C O' a a
+ (mk_is_bounded_above C O' a m H))));
+ assumption
+ ].
+qed.
+
+definition is_sequentially_monotone ≝
+ λC.λO:ordered_set C.λf:O→O.
+ ∀a:nat→O.∀p:is_increasing ? ? a.
+ is_increasing ? ? (λi.f (a i)).
+
+record is_order_continuous (C)
+ (O:dedekind_sigma_complete_ordered_set C) (f:O→O) : Prop
+≝
+ { ioc_is_sequentially_monotone: is_sequentially_monotone ? ? f;
+ ioc_is_upper_bound_f_sup:
+ ∀a:bounded_above_sequence ? O.
+ is_upper_bound ? ? (λi.f (a i)) (f (sup ? ? a));
+ ioc_respects_sup:
+ ∀a:bounded_above_sequence ? O.
+ is_increasing ? ? a →
+ f (sup ? ? a) =
+ sup ? ? (mk_bounded_above_sequence ? ? (λi.f (a i))
+ (mk_is_bounded_above ? ? ? (f (sup ? ? a))
+ (ioc_is_upper_bound_f_sup a)));
+ ioc_is_lower_bound_f_inf:
+ ∀a:bounded_below_sequence ? O.
+ is_lower_bound ? ? (λi.f (a i)) (f (inf ? ? a));
+ ioc_respects_inf:
+ ∀a:bounded_below_sequence ? O.
+ is_decreasing ? ? a →
+ f (inf ? ? a) =
+ inf ? ? (mk_bounded_below_sequence ? ? (λi.f (a i))
+ (mk_is_bounded_below ? ? ? (f (inf ? ? a))
+ (ioc_is_lower_bound_f_inf a)))
+ }.
+
+theorem tail_inf_increasing:
+ ∀C.∀O:dedekind_sigma_complete_ordered_set C.
+ ∀a:bounded_below_sequence ? O.
+ let y ≝ λi.mk_bounded_below_sequence ? ? (λj.a (i+j)) ? in
+ let x ≝ λi.inf ? ? (y i) in
+ is_increasing ? ? x.
+ [ apply (mk_is_bounded_below ? ? ? (ib_lower_bound ? ? a a));
+ simplify;
+ intro;
+ apply (ib_lower_bound_is_lower_bound ? ? a a)
+ | intros;
+ unfold is_increasing;
+ intro;
+ unfold x in ⊢ (? ? ? ? %);
+ apply (inf_greatest_lower_bound ? ? ? ? (inf_is_inf ? ? (y (S n))));
+ change with (is_lower_bound ? ? (y (S n)) (inf ? ? (y n)));
+ unfold is_lower_bound;
+ intro;
+ generalize in match (inf_lower_bound ? ? ? ? (inf_is_inf ? ? (y n)) (S n1));
+ (*CSC: coercion per FunClass inserita a mano*)
+ suppose (inf ? ? (y n) ≤ bbs_seq ? ? (y n) (S n1)) (H);
+ cut (bbs_seq ? ? (y n) (S n1) = bbs_seq ? ? (y (S n)) n1);
+ [ rewrite < Hcut;
+ assumption
+ | unfold y;
+ simplify;
+ auto paramodulation library
+ ]
+ ].
+qed.
+
+definition is_liminf:
+ ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C.
+ bounded_below_sequence ? O → O → Prop.
+ intros;
+ apply
+ (is_sup ? ? (λi.inf ? ? (mk_bounded_below_sequence ? ? (λj.b (i+j)) ?)) t);
+ apply (mk_is_bounded_below ? ? ? (ib_lower_bound ? ? b b));
+ simplify;
+ intros;
+ apply (ib_lower_bound_is_lower_bound ? ? b b).
+qed.
+
+definition liminf:
+ ∀C:Type.∀O:dedekind_sigma_complete_ordered_set C.
+ bounded_sequence ? O → O.
+ intros;
+ apply
+ (sup ? ?
+ (mk_bounded_above_sequence ? ?
+ (λi.inf ? ?
+ (mk_bounded_below_sequence ? ?
+ (λj.b (i+j)) ?)) ?));
+ [ apply (mk_is_bounded_below ? ? ? (ib_lower_bound ? ? b b));
+ simplify;
+ intros;
+ apply (ib_lower_bound_is_lower_bound ? ? b b)
+ | apply (mk_is_bounded_above ? ? ? (ib_upper_bound ? ? b b));
+ unfold is_upper_bound;
+ intro;
+ change with
+ (inf C O
+ (mk_bounded_below_sequence C O (\lambda j:nat.b (n+j))
+ (mk_is_bounded_below C O (\lambda j:nat.b (n+j)) (ib_lower_bound C O b b)
+ (\lambda j:nat.ib_lower_bound_is_lower_bound C O b b (n+j))))
+\leq ib_upper_bound C O b b);
+ apply (inf_respects_le ? O);
+ simplify;
+ intro;
+ apply (ib_upper_bound_is_upper_bound ? ? b b)
+ ].
+qed.
+
+notation "hvbox(〈a〉)"
+ non associative with precedence 45
+for @{ 'hide_everything_but $a }.
+
+interpretation "mk_bounded_above_sequence" 'hide_everything_but a
+= (cic:/matita/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
+
+interpretation "mk_bounded_below_sequence" 'hide_everything_but a
+= (cic:/matita/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
+
+theorem eq_f_sup_sup_f:
+ ∀C.∀O':dedekind_sigma_complete_ordered_set C.
+ ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
+ ∀a:bounded_above_sequence ? O'.
+ ∀p:is_increasing ? ? a.
+ f (sup ? ? a) = sup ? ? (mk_bounded_above_sequence ? ? (λi.f (a i)) ?).
+ [ apply (mk_is_bounded_above ? ? ? (f (sup ? ? a)));
+ apply ioc_is_upper_bound_f_sup;
+ assumption
+ | intros;
+ apply ioc_respects_sup;
+ assumption
+ ].
+qed.
+
+theorem eq_f_sup_sup_f':
+ ∀C.∀O':dedekind_sigma_complete_ordered_set C.
+ ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
+ ∀a:bounded_above_sequence ? O'.
+ ∀p:is_increasing ? ? a.
+ ∀p':is_bounded_above ? ? (λi.f (a i)).
+ f (sup ? ? a) = sup ? ? (mk_bounded_above_sequence ? ? (λi.f (a i)) p').
+ intros;
+ rewrite > (eq_f_sup_sup_f ? ? f H a H1);
+ apply sup_proof_irrelevant;
+ reflexivity.
+qed.
+
+theorem eq_f_liminf_sup_f_inf:
+ ∀C.∀O':dedekind_sigma_complete_ordered_set C.
+ ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
+ ∀a:bounded_sequence ? O'.
+ let p1 := ? in
+ f (liminf ? ? a) =
+ sup ? ?
+ (mk_bounded_above_sequence ? ?
+ (λi.f (inf ? ?
+ (mk_bounded_below_sequence ? ?
+ (λj.a (i+j))
+ ?)))
+ p1).
+ [ apply (mk_is_bounded_below ? ? ? (ib_lower_bound ? ? a a));
+ simplify;
+ intro;
+ apply (ib_lower_bound_is_lower_bound ? ? a a)
+ | apply (mk_is_bounded_above ? ? ? (f (sup ? ? a)));
+ unfold is_upper_bound;
+ intro;
+ apply (or_transitive ? ? O' ? (f (a n)));
+ [ generalize in match (ioc_is_lower_bound_f_inf ? ? ? H);
+ intro H1;
+ simplify in H1;
+ rewrite > (plus_n_O n) in ⊢ (? ? ? ? (? (? ? ? ? %)));
+ apply (H1 (mk_bounded_below_sequence C O' (\lambda j:nat.a (n+j))
+(mk_is_bounded_below C O' (\lambda j:nat.a (n+j)) (ib_lower_bound C O' a a)
+ (\lambda j:nat.ib_lower_bound_is_lower_bound C O' a a (n+j)))) O);
+ | elim daemon (*apply (ioc_is_upper_bound_f_sup ? ? ? H)*)
+ ]
+ | intros;
+ unfold liminf;
+ clearbody p1;
+ generalize in match (\lambda n:nat
+.inf_respects_le C O'
+ (mk_bounded_below_sequence C O' (\lambda j:nat.a (plus n j))
+ (mk_is_bounded_below C O' (\lambda j:nat.a (plus n j))
+ (ib_lower_bound C O' a a)
+ (\lambda j:nat.ib_lower_bound_is_lower_bound C O' a a (plus n j))))
+ (ib_upper_bound C O' a a)
+ (\lambda n1:nat.ib_upper_bound_is_upper_bound C O' a a (plus n n1)));
+ intro p2;
+ apply (eq_f_sup_sup_f' ? ? f H (mk_bounded_above_sequence C O'
+(\lambda i:nat
+ .inf C O'
+ (mk_bounded_below_sequence C O' (\lambda j:nat.a (plus i j))
+ (mk_is_bounded_below C O' (\lambda j:nat.a (plus i j))
+ (ib_lower_bound C O' a a)
+ (\lambda n:nat.ib_lower_bound_is_lower_bound C O' a a (plus i n)))))
+(mk_is_bounded_above C O'
+ (\lambda i:nat
+ .inf C O'
+ (mk_bounded_below_sequence C O' (\lambda j:nat.a (plus i j))
+ (mk_is_bounded_below C O' (\lambda j:nat.a (plus i j))
+ (ib_lower_bound C O' a a)
+ (\lambda n:nat.ib_lower_bound_is_lower_bound C O' a a (plus i n)))))
+ (ib_upper_bound C O' a a) p2)));
+ unfold bas_seq;
+ change with
+ (is_increasing ? ? (\lambda i:nat
+.inf C O'
+ (mk_bounded_below_sequence C O' (\lambda j:nat.a (plus i j))
+ (mk_is_bounded_below C O' (\lambda j:nat.a (plus i j))
+ (ib_lower_bound C O' a a)
+ (\lambda n:nat.ib_lower_bound_is_lower_bound C O' a a (plus i n))))));
+ apply tail_inf_increasing
+ ].
+qed.
+
+
+
+
+definition lt ≝ λC.λO:ordered_set C.λa,b:O.a ≤ b ∧ a ≠ b.
+
+interpretation "Ordered set lt" 'lt a b =
+ (cic:/matita/ordered_sets/lt.con _ _ a b).
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/ordered_sets2".
+
+include "ordered_sets.ma".
+
+theorem le_f_inf_inf_f:
+ ∀C.∀O':dedekind_sigma_complete_ordered_set C.
+ ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
+ ∀a:bounded_below_sequence ? O'.
+ let p := ? in
+ f (inf ? ? a) ≤ inf ? ? (mk_bounded_below_sequence ? ? (λi. f (a i)) p).
+ [ apply mk_is_bounded_below;
+ [2: apply ioc_is_lower_bound_f_inf;
+ assumption
+ | skip
+ ]
+ | intros;
+ clearbody p;
+ apply (inf_greatest_lower_bound ? ? ? ? (inf_is_inf ? ? ?));
+ simplify;
+ intro;
+ letin b := (λi.match i with [ O ⇒ inf ? ? a | S _ ⇒ a n]);
+ change with (f (b O) ≤ f (b (S O)));
+ apply (ioc_is_sequentially_monotone ? ? ? H);
+ simplify;
+ clear b;
+ intro;
+ elim n1; simplify;
+ [ apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? ?));
+ | apply (or_reflexive ? O' (dscos_ordered_set ? O'))
+ ]
+ ].
+qed.
+
+theorem le_to_le_sup_sup:
+ ∀C.∀O':dedekind_sigma_complete_ordered_set C.
+ ∀a,b:bounded_above_sequence ? O'.
+ (∀i.a i ≤ b i) → sup ? ? a ≤ sup ? ? b.
+ intros;
+ apply (sup_least_upper_bound ? ? ? ? (sup_is_sup ? ? a));
+ unfold;
+ intro;
+ apply (or_transitive ? ? O');
+ [2: apply H
+ | skip
+ | apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? b))
+ ].
+qed.
+
+interpretation "mk_bounded_sequence" 'hide_everything_but a
+= (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
+
+theorem fatou:
+ ∀C.∀O':dedekind_sigma_complete_ordered_set C.
+ ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
+ ∀a:bounded_sequence ? O'.
+ let pb := ? in
+ let pa := ? in
+ f (liminf ? ? a) ≤ liminf ? ? (mk_bounded_sequence ? ? (λi. f (a i)) pb pa).
+ [ letin bas ≝ (bounded_above_sequence_of_bounded_sequence ? ? a);
+ apply mk_is_bounded_above;
+ [2: apply (ioc_is_upper_bound_f_sup ? ? ? H bas)
+ | skip
+ ]
+ | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? ? a);
+ apply mk_is_bounded_below;
+ [2: apply (ioc_is_lower_bound_f_inf ? ? ? H bbs)
+ | skip
+ ]
+ | intros;
+ rewrite > eq_f_liminf_sup_f_inf;
+ [ unfold liminf;
+ apply le_to_le_sup_sup;
+ elim daemon (*(* f inf < inf f *)
+ apply le_f_inf_inf_f*)
+ | assumption
+ ]
+ ].
+qed.
definition max_seq: ∀R:real.∀x,y:R. nat → R.
intros (R x y);
- elim (to_cotransitive R (of_le R) R 0 (inv ? (sum_field ? (S n)) ?) (x-y));
+ elim (of_cotransitive R 0 (inv ? (sum_field ? (S n)) ?) (x-y));
[ apply x
| apply not_eq_sum_field_zero ;
unfold;
axiom daemon: False.
theorem cauchy_max_seq: ∀R:real.∀x,y:R. is_cauchy_seq ? (max_seq ? x y).
+elim daemon.
+(*
intros;
unfold;
intros;
exists; [ exact m | ]; (* apply (ex_intro ? ? m); *)
intros;
unfold max_seq;
- elim (to_cotransitive R (of_le R) R 0
+ elim (of_cotransitive R 0
(inv R (sum_field R (S N))
(not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))) (x-y)
(lt_zero_to_le_inv_zero R (S N)
(not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))));
[ simplify;
- elim (to_cotransitive R (of_le R) R 0
+ elim (of_cotransitive R 0
(inv R (1+sum R (plus R) 0 1 m)
(not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
(lt_zero_to_le_inv_zero R (S m)
]
| simplify;
split;
- [ apply (to_transitive ? ?
- (of_total_order_relation ? ? R) ? 0 ?);
- [ apply (le_zero_x_to_le_opp_x_zero R ?)
- | assumption
- ]
+ [ apply (or_transitive ? ? R ? 0);
+ [ apply (le_zero_x_to_le_opp_x_zero R ?)
+ | assumption
+ ]
| assumption
]
]
| simplify;
- elim (to_cotransitive R (of_le R) R 0
+ elim (of_cotransitive R 0
(inv R (1+sum R (plus R) 0 1 m)
(not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
(lt_zero_to_le_inv_zero R (S m)
rewrite > eq_opp_plus_plus_opp_opp in H1;
rewrite > eq_opp_opp_x_x in H1;
rewrite > plus_comm in H1;
- apply (to_transitive ? ? (of_total_order_relation ? ? R) ? 0 ?);
+ apply (or_transitive ? ? R ? 0);
[ assumption
| apply lt_zero_to_le_inv_zero
]
]
]
].
- elim daemon.
+ elim daemon.*)
qed.
definition max: ∀R:real.R → R → R.
elim daemon.
qed.
-lemma abs_x_ge_O: \forall R: real. \forall x:R. 0 ≤ abs R x.
+lemma abs_x_ge_O: \forall R: real. \forall x:R. (zero R) ≤ abs R x.
intros;
unfold abs;
unfold max;
unfold to_zero;
unfold max_seq;
elim
- (to_cotransitive R (of_le R) R 0
+ (of_cotransitive R 0
(inv R (sum_field R (S n))
(not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))) (x--x)
(lt_zero_to_le_inv_zero R (S n)
generalize in match (zero_neutral R 0);
intro;
generalize in match (eq_f ? ? (λy.x*y) ? ? H); intro; clear H;
-rewrite > mult_plus_distr_left in H1;
+(*CSC: qua funzionava prima della patch all'unificazione!*)
+rewrite > (mult_plus_distr_left R) in H1;
generalize in match (eq_f ? ? (λy. (-(x*0)) +y) ? ? H1);intro;
clear H1;
rewrite < plus_assoc in H;
(cic:/matita/vector_spaces/emult.con _ _ a b).
record is_semi_norm (R:real) (V: vector_space R) (semi_norm:V→R) : Prop \def
- { sn_positive: ∀x:V. 0 ≤ semi_norm x;
+ { sn_positive: ∀x:V. zero R ≤ semi_norm x;
sn_omogeneous: ∀a:R.∀x:V. semi_norm (a*x) = (abs ? a) * semi_norm x;
sn_triangle_inequality: ∀x,y:V. semi_norm (x + y) ≤ semi_norm x + semi_norm y
}.
}.
record is_semi_distance (R:real) (C:Type) (semi_d: C→C→R) : Prop ≝
- { sd_positive: ∀x,y:C. 0 ≤ semi_d x y;
+ { sd_positive: ∀x,y:C. zero R ≤ semi_d x y;
sd_properness: ∀x:C. semi_d x x = 0;
sd_triangle_inequality: ∀x,y,z:C. semi_d x z ≤ semi_d x y + semi_d z y
}.
theorem induced_distance_is_distance:
∀R:real.∀V:vector_space R.∀norm:norm ? V.
is_distance ? ? (induced_distance_fun ? ? norm).
+elim daemon.(*
intros;
apply mk_is_distance;
[ apply mk_is_semi_distance;
elim daemon
| apply (n_norm_properties ? ? norm)
]
- ].
+ ].*)
qed.
definition induced_distance ≝
definition tends_to :
∀R:real.∀V:vector_space R.∀d:distance ? V.∀f:nat→V.∀l:V.Prop.
- alias symbol "leq" = "Ordered field le".
- alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
apply
(λR:real.λV:vector_space R.λd:distance ? V.λf:nat→V.λl:V.
∀n:nat.∃m:nat.∀j:nat. le m j →
projects / helm.git / commitdiff