From 951decc20babd2704b82faa8922684f2dee21cdc Mon Sep 17 00:00:00 2001 From: grunweg Date: Tue, 5 Mar 2024 23:12:06 +0000 Subject: [PATCH] style: remove three double spaces (#11186) --- Mathlib/Data/List/NodupEquivFin.lean | 4 ++-- Mathlib/GroupTheory/Submonoid/Membership.lean | 2 +- Mathlib/Order/PartialSups.lean | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Data/List/NodupEquivFin.lean b/Mathlib/Data/List/NodupEquivFin.lean index 187d9aac4894df..533e49acc9e578 100644 --- a/Mathlib/Data/List/NodupEquivFin.lean +++ b/Mathlib/Data/List/NodupEquivFin.lean @@ -19,8 +19,8 @@ Given a list `l`, sending `⟨x, hx⟩` to `⟨indexOf x l, _⟩`; * if `l` has no duplicates and contains every element of a type `α`, then - `List.Nodup.getEquivOfForallMemList` defines an equivalence between - `Fin (length l)` and `α`; if `α` does not have decidable equality, then + `List.Nodup.getEquivOfForallMemList` defines an equivalence between `Fin (length l)` and `α`; + if `α` does not have decidable equality, then there is a bijection `List.Nodup.getBijectionOfForallMemList`; * if `l` is sorted w.r.t. `(<)`, then `List.Sorted.getIso` is the same bijection reinterpreted diff --git a/Mathlib/GroupTheory/Submonoid/Membership.lean b/Mathlib/GroupTheory/Submonoid/Membership.lean index 3d3dbbd5e10f27..a2c7effd100990 100644 --- a/Mathlib/GroupTheory/Submonoid/Membership.lean +++ b/Mathlib/GroupTheory/Submonoid/Membership.lean @@ -371,7 +371,7 @@ theorem card_le_one_iff_eq_bot : card S ≤ 1 ↔ S = ⊥ := @[to_additive] lemma eq_bot_iff_card : S = ⊥ ↔ card S = 1 := - ⟨by rintro rfl; exact card_bot, eq_bot_of_card_eq⟩ + ⟨by rintro rfl; exact card_bot, eq_bot_of_card_eq⟩ end Submonoid diff --git a/Mathlib/Order/PartialSups.lean b/Mathlib/Order/PartialSups.lean index 783bb5a17e3d1b..d454e9edaf5249 100644 --- a/Mathlib/Order/PartialSups.lean +++ b/Mathlib/Order/PartialSups.lean @@ -61,7 +61,7 @@ theorem partialSups_succ (f : ℕ → α) (n : ℕ) : #align partial_sups_succ partialSups_succ lemma partialSups_iff_forall {f : ℕ → α} (p : α → Prop) - (hp : ∀ {a b}, p (a ⊔ b) ↔ p a ∧ p b) : ∀ {n : ℕ}, p (partialSups f n) ↔ ∀ k ≤ n, p (f k) + (hp : ∀ {a b}, p (a ⊔ b) ↔ p a ∧ p b) : ∀ {n : ℕ}, p (partialSups f n) ↔ ∀ k ≤ n, p (f k) | 0 => by simp | (n + 1) => by simp [hp, partialSups_iff_forall, ← Nat.lt_succ_iff, ← Nat.forall_lt_succ]