.

EvgenyMakarov · Jan 29, 2013 · 52cff51 · 52cff51
1 parent 4dfdc13
commit 52cff51
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/broken/BanachFixpoint.v b/broken/BanachFixpoint.v
@@ -199,8 +199,6 @@ end.
   - intros; apply mspc_symm; now apply A.
 Qed.
 
-SearchAbout (?x = ?y ∨ ?x < ?y).
-
 Let a := lim (reg_fun x _ cauchy_x).
 
 Lemma banach_fixpoint : f a = a.

diff --git a/broken/metric.v b/broken/metric.v
@@ -630,7 +630,7 @@ constructor.
 + intros z1 z2 e [A1 A2].
   (* Below we prove [0 ≤ e] using [radius_nonneg], which requires
   [ExtMetricSpaceClass]. Another way is to add the assymption [0 ≤ e] to
-  [lip_prf], sinilar to [uc_prf]. *)
+  [lip_prf], similar to [uc_prf]. *)
   assert (0 ≤ e) by now apply (radius_nonneg (fst z1) (fst z2)).
   split; simpl.
   - apply (mspc_monotone (L1 * e)); [apply (order_preserving (.* e)); apply join_ub_l |].