Skip to content

Section 9.3: remove unnecessary AdherentPt hypotheses and fix statements#484

Open
rkirov wants to merge 1 commit intoteorth:mainfrom
rkirov:upstream-statement-fixes
Open

Section 9.3: remove unnecessary AdherentPt hypotheses and fix statements#484
rkirov wants to merge 1 commit intoteorth:mainfrom
rkirov:upstream-statement-fixes

Conversation

@rkirov
Copy link
Copy Markdown
Contributor

@rkirov rkirov commented Apr 11, 2026

Remark 9.3.11 asked whether the AdherentPt hypothesis could be removed from Proposition 9.3.9 and subsequent theorems. Formalization confirms it can. This removes AdherentPt from 17 theorem statements (keeping it only in Convergesto.uniq where it is genuinely needed).

Other statement fixes:

  • Example 9.3.2 constants: 5 → 5.1, 0.41 → 0.42 (needed for strict <)
  • sq, linear, quadratic: fix argument order (limit before point)
  • const, id, sq, linear, quadratic: implicit → explicit args
  • const body: fun x ↦ c → fun _ ↦ c

Comment thread Analysis/Section_9_3.lean
rw [iff_conv f L] at hf; solve_by_elim

-- Remark 9.3.11 may possibly be inaccurate, in that one may be able to safely delete the hypothesis `AdherentPt x₀ E` in the above theorems. This is something that formalization might be able to clarify! If so, the hypothesis may also be deletable in several of the theorems below.
-- Remark 9.3.11 is not quite true in Lean: the hypothesis `AdherentPt x₀ E` is safely removed
Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

all theorems proved without the Adherent condition - https://github.com/rkirov/analysis/blob/main/Analysis/Section_9_3.lean

@rkirov
Copy link
Copy Markdown
Contributor Author

rkirov commented Apr 11, 2026

Removing AdherentPt hypothesis caused some downstream breakages that I am working through now

Remark 9.3.11 asked whether the AdherentPt hypothesis could be removed
from Proposition 9.3.9 and subsequent theorems. Formalization confirms
it can. This removes AdherentPt from 17 theorem statements (keeping it
only in Convergesto.uniq where it is genuinely needed).

Other statement fixes:
- Example 9.3.2 constants: 5 → 5.1, 0.41 → 0.42 (needed for strict <)
- sq, linear, quadratic: fix argument order (limit before point)
- const, id, sq, linear, quadratic: implicit → explicit args
- const body: fun x ↦ c → fun _ ↦ c

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@rkirov rkirov force-pushed the upstream-statement-fixes branch from bfb9358 to 76cf7ab Compare April 11, 2026 15:39
@rkirov
Copy link
Copy Markdown
Contributor Author

rkirov commented Apr 11, 2026

Removing AdherentPt hypothesis caused some downstream breakages that I am working through now

Should be good to review now.

Sign up for free to 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.

1 participant