Skip to content

fix: disambiguate duplicate Verso labels in Section 6.2 - #654

Open
Chessing234 wants to merge 2 commits into
teorth:mainfrom
Chessing234:fix/section-6-2-verso-labels
Open

fix: disambiguate duplicate Verso labels in Section 6.2#654
Chessing234 wants to merge 2 commits into
teorth:mainfrom
Chessing234:fix/section-6-2-verso-labels

Conversation

@Chessing234

Copy link
Copy Markdown
Contributor

Section 6.2 has three groups of declarations sharing one docstring:

  • Definition 6.2.3 (Ordering of extended reals) — 2 (the and < characterisations)
  • Examples 6.2.4 — 4 examples
  • Definition 6.2.6 — 5 theorems covering the different supremum cases

Same convention as #624: the definitions name the case they cover ((supremum of the empty set), (supremum ignores negative infinity), …), the examples take part letters as in #634. Docstrings only.

Checked: no duplicate one-line docstrings remain, all edited lines within 100 characters.

lake build Analysis.Section_6_2 succeeds locally — Build completed successfully (3273 jobs). The one info: line it prints is a pre-existing #check-style trace at Section_6_2.lean:177, unrelated to this change.

Eleven docstrings across three groups shared a label: Definition 6.2.3,
Examples 6.2.4 and Definition 6.2.6.
The two ordering definitions and the five supremum cases name what they cover;
the four examples take part letters.
@teorth

Copy link
Copy Markdown
Owner

Thanks — the Definition 6.2.3 and Definition 6.2.6 disambiguators are exactly the right style, and I've merged the sibling PRs that use it throughout.

One thing to adjust first. Examples 6.2.4 is a single prose sentence in ch6, not an enumerated list:

$3 \leq 5$, $3 &lt; +\infty$, and $-\infty &lt; +\infty$, but $3 \not\leq -\infty$.

There are no parts (a)–(d) in the text, so labelling the four Lean examples that way asserts structure the book doesn't have. Could you switch to descriptive parentheticals, matching the style you used for Definition 6.2.3 in the same PR? For instance (two reals), (a real and positive infinity), (negative and positive infinity), (a real is not below negative infinity).

The rest is good to merge.

Examples 6.2.4 is a single prose sentence in the text with no parts
(a)-(d), so the enumerated labels asserted structure the book does not
have. Use the same descriptive style as Definition 6.2.3 in this PR.
@Chessing234

Copy link
Copy Markdown
ContributorAuthor

Done in 37af0f0Examples 6.2.4 now reads (two reals), (a real and positive infinity), (negative and positive infinity), (a real is not below negative infinity), matching the order of the four examples. The Definition 6.2.3/6.2.6 labels are unchanged.

Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants

@Chessing234@teorth