fix(*): replace "the the" by "the" (#10548)

leanprover-community · Nov 30, 2021 · 35574bb · 35574bb
1 parent 1077f34
commit 35574bb
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/linear_algebra/affine_space/basis.lean b/src/linear_algebra/affine_space/basis.lean
@@ -234,7 +234,7 @@ begin
 end
 
 /-- Given a family of points `p : ι' → P` and an affine basis `b`, if the matrix whose rows are the
-coordinates of `p` with respect `b` has a left inverse, then `p` spans the the entire space. -/
+coordinates of `p` with respect `b` has a left inverse, then `p` spans the entire space. -/
 lemma affine_span_eq_top_of_to_matrix_left_inv [decidable_eq ι] [nontrivial k]
   (p : ι' → P) {A : matrix ι ι' k} (hA : A ⬝ b.to_matrix p = 1) : affine_span k (range p) = ⊤ :=
 begin

diff --git a/src/topology/sheaves/sheaf_condition/sites.lean b/src/topology/sheaves/sheaf_condition/sites.lean
@@ -317,7 +317,7 @@ pi.lift (λ f, pi.π _ (index_of_hom U f) ≫ F.map (eq_to_hom (index_of_hom_spe
 Even though `first_obj_to_pi_opens` and `pi_opens_to_first_obj` are not inverse to each other,
 applying them both after a fork map `s.ι` does nothing. The intuition here is that a compatible
 family `s : Π i : ι, F.obj (op (U i))` does not care about duplicate open sets:
-If `U i = U j` the the compatible family coincides on the intersection `U i ⊓ U j = U i = U j`,
+If `U i = U j` the compatible family coincides on the intersection `U i ⊓ U j = U i = U j`,
 hence `s i = s j` (module an `eq_to_hom` arrow).
 -/
 lemma fork_ι_comp_pi_opens_to_first_obj_to_pi_opens_eq