From 4be31ef7f08fd8984b3fb2e490054e4065cf9b71 Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 31 Jul 2026 14:15:52 +0300 Subject: [PATCH] fix: space Verso docstring closers; correct BddAbove/Below comments Insert the missing space before `-/` in several module docs, and fix "if X if not BddBelow" / "Bddabove" wording in Section_1_1_1. Co-authored-by: Cursor --- Analysis/MeasureTheory/Section_1_1_1.lean | 4 ++-- Analysis/Section_11_3.lean | 2 +- Analysis/Section_11_4.lean | 2 +- Analysis/Section_2_2.lean | 4 ++-- Analysis/Section_3_4.lean | 2 +- Analysis/Section_8_2.lean | 4 ++-- 6 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_1.lean b/Analysis/MeasureTheory/Section_1_1_1.lean index e7014cf81..bbe2b72df 100644 --- a/Analysis/MeasureTheory/Section_1_1_1.lean +++ b/Analysis/MeasureTheory/Section_1_1_1.lean @@ -289,12 +289,12 @@ def witness_upperBound_lowerBounds {X : Set ℝ} (y : ℝ) (hy : y ∈ X) /- If x < sSup X and X is not empty, then there exists z ∈ X with x < z -/ /- We don't need to assume that X is BddAbove --(if X is not Bddabove, we get that sSup X = 0 (the junk value) and the result still follows -/ +-(if X is not BddAbove, we get that sSup X = 0 (the junk value) and the result still follows -/ #check exists_lt_of_lt_csSup /- If sInf X < x and X is not empty, then there exists w ∈ X with w ≤ x -/ /- We don't need to assume that X is BddBelow. --(if X if not BddBelow, we get that sInf X = 0 (the junk value) and the result still follows-/ +-(if X is not BddBelow, we get that sInf X = 0 (the junk value) and the result still follows -/ #check exists_lt_of_csInf_lt /-- Show x < b when b = sSup X and b ∉ X -/ diff --git a/Analysis/Section_11_3.lean b/Analysis/Section_11_3.lean index cb0b8763a..527097422 100644 --- a/Analysis/Section_11_3.lean +++ b/Analysis/Section_11_3.lean @@ -120,7 +120,7 @@ lemma gt_of_lt_lower_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f simp at hY; peel hY; simp_all; tauto /-- Definition 11.3.4 (Riemann integral) -As we permit junk values, the simplest definition for the Riemann integral is the upper integral.-/ +As we permit junk values, the simplest definition for the Riemann integral is the upper integral. -/ noncomputable abbrev integ (f:ℝ → ℝ) (I: BoundedInterval) : ℝ := upper_integral f I theorem integ_congr {f g:ℝ → ℝ} {I: BoundedInterval} (h: Set.EqOn f g I) : diff --git a/Analysis/Section_11_4.lean b/Analysis/Section_11_4.lean index b7c9201b3..c217c2311 100644 --- a/Analysis/Section_11_4.lean +++ b/Analysis/Section_11_4.lean @@ -157,7 +157,7 @@ theorem IntegrableOn.abs {I: BoundedInterval} {f:ℝ → ℝ} (hf: IntegrableOn ext x; obtain h | h := (show f x ≤ 0 ∨ f x ≥ 0 by grind) <;> simp [h] /-- Theorem 11.4.5 (Products preserve Riemann integrability). -It is convenient to first establish the non-negative case.-/ +It is convenient to first establish the non-negative case. -/ theorem integ_of_mul_nonneg {I: BoundedInterval} {f g:ℝ → ℝ} (hf: IntegrableOn f I) (hg: IntegrableOn g I) (hf_nonneg: MajorizesOn f 0 I) (hg_nonneg: MajorizesOn g 0 I) : IntegrableOn (f * g) I := by diff --git a/Analysis/Section_2_2.lean b/Analysis/Section_2_2.lean index 32076d441..14eed0769 100644 --- a/Analysis/Section_2_2.lean +++ b/Analysis/Section_2_2.lean @@ -38,7 +38,7 @@ namespace Chapter2 abbrev Nat.add (n m : Nat) : Nat := Nat.recurse (fun _ sum ↦ sum++) m n /-- This instance allows for the {kw (of := «term_+_»)}`+` notation to be used for natural number - addition.-/ + addition. -/ instance Nat.instAdd : Add Nat where add := add /-- Compare with Mathlib's {name}`Nat.zero_add`. -/ @@ -225,7 +225,7 @@ theorem Nat.succ_gt_self (n:Nat) : n++ > n := by /-- Proposition 2.2.12 (Basic properties of order for natural numbers) / Exercise 2.2.3 -(a) (Order is reflexive). Compare with Mathlib's {name}`Nat.le_refl`.-/ +(a) (Order is reflexive). Compare with Mathlib's {name}`Nat.le_refl`. -/ theorem Nat.ge_refl (a:Nat) : a ≥ a := by sorry diff --git a/Analysis/Section_3_4.lean b/Analysis/Section_3_4.lean index 4cceab488..e27e95fa1 100644 --- a/Analysis/Section_3_4.lean +++ b/Analysis/Section_3_4.lean @@ -276,7 +276,7 @@ Interestingly, it is not needed for U to be a subset of Y. -/ -- theorem SetTheory.Set.image_of_preimage {X Y:Set} (f:X → Y) (U: Set) : sorry := by sorry /- Exercise 3.4.2. State and prove an assertion connecting `preimage f (image f (preimage f U))` and `preimage f U`. -Interestingly, it is not needed for U to be a subset of Y.-/ +Interestingly, it is not needed for U to be a subset of Y. -/ -- theorem SetTheory.Set.preimage_of_image_of_preimage {X Y:Set} (f:X → Y) (U: Set) : sorry := by sorry /-- diff --git a/Analysis/Section_8_2.lean b/Analysis/Section_8_2.lean index f34fc1c71..9d9640f26 100644 --- a/Analysis/Section_8_2.lean +++ b/Analysis/Section_8_2.lean @@ -31,7 +31,7 @@ open Chapter7 Chapter7.Series Finset Function Filter /-- Definition 8.2.1 (Series on countable sets). Note that with this definition, functions defined on finite sets will not be absolutely convergent; one should use {lit}`AbsConvergent'` instead for such -cases.-/ +cases. -/ abbrev AbsConvergent {X:Type} (f: X → ℝ) : Prop := ∃ g: ℕ → X, Bijective g ∧ (f ∘ g: Series).absConverges theorem AbsConvergent.mk {X: Type} {f:X → ℝ} {g:ℕ → X} (h: Bijective g) (hfg: (f ∘ g:Series).absConverges) : AbsConvergent f := by use g @@ -434,7 +434,7 @@ theorem Sum'.of_disjoint_union {X:Type} {f:X → ℝ} (hf: AbsConvergent' f) {X sorry /-- This technical claim, the analogue of {name}`tsum_univ`, is required due to the way Mathlib handles - sets.-/ + sets. -/ theorem Sum'.of_univ {X:Type} {f:X → ℝ} (hf: AbsConvergent' f) : Sum' (fun x: (.univ : Set X) ↦ f x) = Sum' f := by sorry