X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fordered_uniform.ma;h=701651cb1160a68c4ecd2142ba4477d0fcc92d40;hb=82d281529c1a9450ac213a058e7f8c0e228026fa;hp=0bc8a32255cde1804c708a588c4f25f772215ed6;hpb=f36588e673e67f0758fdbec52baa515a28fd9a7a;p=helm.git diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma index 0bc8a3225..701651cb1 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma @@ -37,19 +37,6 @@ record ordered_uniform_space : Type ≝ { ous_convex: ∀U.us_unifbase ous_stuff U → convex ous_stuff U }. -definition Type_of_ordered_uniform_space : ordered_uniform_space → Type. -intro; compose ordered_set_OF_ordered_uniform_space with os_l. -apply (hos_carr (f o)); -qed. - -definition Type_of_ordered_uniform_space_dual : ordered_uniform_space → Type. -intro; compose ordered_set_OF_ordered_uniform_space with os_r. -apply (hos_carr (f o)); -qed. - -coercion Type_of_ordered_uniform_space. -coercion Type_of_ordered_uniform_space_dual. - definition half_ordered_set_OF_ordered_uniform_space : ordered_uniform_space → half_ordered_set. intro; compose ordered_set_OF_ordered_uniform_space with os_l. apply (f o); qed. @@ -114,24 +101,6 @@ lemma bs2_of_bss2: coercion bs2_of_bss2 nocomposites. -(* -notation < "x \sub \neq" with precedence 91 for @{'bsss $x}. -interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x). -*) - -(* -lemma ss_of_bs: - ∀O:ordered_set.∀u,v:O. - ∀b:O squareO.\fst b ∈ [u,v] → \snd b ∈ [u,v] → {[u,v]} squareO ≝ - λO:ordered_set.λu,v:O. - λb:O squareB.λH1,H2.〈≪\fst b,H1≫,≪\snd b,H2≫〉. -*) - -(* -notation < "x \sub \nleq" with precedence 91 for @{'ssbs $x}. -interpretation "ss_of_bs" 'ssbs x = (ss_of_bs _ _ _ x _ _). -*) - lemma segment_ordered_uniform_space: ∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space. intros (O l r); apply mk_ordered_uniform_space; @@ -143,39 +112,39 @@ intros (O l r); apply mk_ordered_uniform_space; [1: intros (U H); intro x; simplify; cases H (w Hw); cases Hw (Gw Hwp); clear H Hw; intro Hm; lapply (us_phi1 O w Gw x Hm) as IH; - apply (restrict ? l r ??? Hwp IH); STOP + apply (restrict ? l r ??? Hwp IH); |2: intros (U V HU HV); cases HU (u Hu); cases HV (v Hv); clear HU HV; cases Hu (Gu HuU); cases Hv (Gv HvV); clear Hu Hv; - cases (us_phi2 ??? Gu Gv) (w HW); cases HW (Gw Hw); clear HW; - exists; [apply (λb:{[l,r]} square.w b)] split; + cases (us_phi2 O u v Gu Gv) (w HW); cases HW (Gw Hw); clear HW; + exists; [apply (λb:{[l,r]} squareB.w b)] split; [1: unfold f; simplify; clearbody f; exists; [apply w]; split; [assumption] intro b; simplify; unfold segment_square_of_ordered_set_square; cases b; intros; split; intros; assumption; |2: intros 2 (x Hx); cases (Hw ? Hx); split; - [apply (restrict ?????? HuU H)|apply (restrict ?????? HvV H1);]] + [apply (restrict O l r ??? HuU H)|apply (restrict O l r ??? HvV H1);]] |3: intros (U Hu); cases Hu (u HU); cases HU (Gu HuU); clear Hu HU; - cases (us_phi3 ?? Gu) (w HW); cases HW (Gw Hwu); clear HW; - exists; [apply (λx:{[l,r]} square.w x)] split; + cases (us_phi3 O u Gu) (w HW); cases HW (Gw Hwu); clear HW; + exists; [apply (λx:{[l,r]} squareB.w x)] split; [1: exists;[apply w];split;[assumption] intros; simplify; intro; unfold segment_square_of_ordered_set_square; cases b; intros; split; intro; assumption; - |2: intros 2 (x Hx); apply (restrict ?????? HuU); apply Hwu; + |2: intros 2 (x Hx); apply (restrict O l r ??? HuU); apply Hwu; cases Hx (m Hm); exists[apply (\fst m)] apply Hm;] |4: intros (U HU x); cases HU (u Hu); cases Hu (Gu HuU); clear HU Hu; - cases (us_phi4 ?? Gu x) (Hul Hur); + cases (us_phi4 O u Gu x) (Hul Hur); split; intros; - [1: lapply (invert_restriction_agreement ????? HuU) as Ra; - apply (restrict ????? x Ra); - apply Hul; apply (unrestrict ?????? HuU H); - |2: apply (restrict ?????? HuU); apply Hur; - apply (unrestrict ?????? (invert_restriction_agreement ????? HuU) H);]] + [1: lapply (invert_restriction_agreement O l r ?? HuU) as Ra; + apply (restrict O l r ?? x Ra); + apply Hul; apply (unrestrict O l r ??? HuU H); + |2: apply (restrict O l r ??? HuU); apply Hur; + apply (unrestrict O l r ??? (invert_restriction_agreement O l r ?? HuU) H);]] |2: simplify; reflexivity;] |2: simplify; unfold convex; intros; cases H (u HU); cases HU (Gu HuU); clear HU H; - lapply (ous_convex ?? Gu (bs_of_ss ? l r p) ? H2 (bs_of_ss ? l r y) H3) as Cu; - [1: apply (unrestrict ?????? HuU); apply H1; - |2: apply (restrict ?????? HuU Cu);]] + lapply (ous_convex ?? Gu p ? H2 y H3) as Cu; + [1: apply (unrestrict O l r ??? HuU); apply H1; + |2: apply (restrict O l r ??? HuU Cu);]] qed. interpretation "Ordered uniform space segment" 'segment_set a b = @@ -187,7 +156,7 @@ lemma restric_uniform_convergence: ∀O:ordered_uniform_space.∀l,u:O. ∀x:{[l,u]}. ∀a:sequence {[l,u]}. - ⌊n,\fst (a n)⌋ uniform_converges (\fst x) → + (⌊n, \fst (a n)⌋ : sequence O) uniform_converges (\fst x) → a uniform_converges x. intros 8; cases H1; cases H2; clear H2 H1; cases (H ? H3) (m Hm); exists [apply m]; intros; @@ -197,3 +166,16 @@ qed. definition order_continuity ≝ λC:ordered_uniform_space.∀a:sequence C.∀x:C. (a ↑ x → a uniform_converges x) ∧ (a ↓ x → a uniform_converges x). + +lemma hint_boh1: ∀O. Type_OF_ordered_uniform_space O → hos_carr (os_l O). +intros; assumption; +qed. + +coercion hint_boh1 nocomposites. + +lemma hint_boh2: ∀O:ordered_uniform_space. hos_carr (os_l O) → Type_OF_ordered_uniform_space O. +intros; assumption; +qed. + +coercion hint_boh2 nocomposites. +