All pull requests

Pull requests

• Add generic facts about einfs and limn_einf

  #2107·lyonel2017 opened Sep 23, 2026Contributor·

  ·

• Add function to restrict a real to the intervale [0 , 1]

  #2106·lyonel2017 opened Sep 23, 2026Contributor·

  ·

• chore: 📝 Links in deflist in Rocqnavi comments

  #2103·yoshihiro503 opened Sep 16, 2026Contributor·

  ·
  15

• open_nbhs -> mem_open

  renaming/refactoring 🔧
  #2094·affeldt-aist opened Aug 30, 2026Member·

  ·

  · 1.19.0
  2

  7

• reversed parameterized integral

  enhancement ✨
  #2091·affeldt-aist opened Aug 23, 2026Member·

  ·

  · 1.19.0
  3

• add Rintegral_gt0 and Rintegral_gt0_itvcc

  #2086·t6s opened Aug 19, 2026Member·

  ·

• Counting distribution

  #2064·lyonel2017 opened Jul 29, 2026Contributor·

  ·

  · 1.19.0
  17

• Counting esum

  #2063·lyonel2017 opened Jul 29, 2026Contributor·

  ·

  · 1.19.0
  3

• Proof of interchange_psum using esum

  #2061·lyonel2017 opened Jul 29, 2026Contributor·

  ·

  · 1.19.0
  8

• experimental_reals: make psumZ rewrite direction explicit

  #2054·JasonGross opened Jul 28, 2026·

  ·

• deflists docs

  #2052·hoheinzollern opened Jul 24, 2026Member·

  ·

• Fix some notation levels w.r.t. Corelib

  #2042·hivert opened Jul 19, 2026Member·

  ·
  1

  4

• Continuity of Rintegral in its bounds

  #2038·amolinamounier opened Jul 15, 2026Collaborator·

  ·

  · 1.19.0

• Rintegral manipulation lemmas

  #2037·amolinamounier opened Jul 15, 2026Collaborator·

  ·

  · 1.19.0

• lemmas around exponential growth

  #2036·amolinamounier opened Jul 15, 2026Collaborator·

  ·

  · 1.19.0

• new series convergence criteria

  #2035·amolinamounier opened Jul 15, 2026Collaborator·

  ·

  · 1.19.0

• L'Hôpital's rule for ∞/∞ forms

  #2034·amolinamounier opened Jul 15, 2026Collaborator·

  ·

  · 1.19.0
  1

• derivable_oo_LRcontinuous stability lemmas

  #2033·amolinamounier opened Jul 15, 2026Collaborator·

  ·

  · 1.19.0

• Derivative limit theorem

  #2032·amolinamounier opened Jul 15, 2026Collaborator·

  ·

  · 1.19.0
  1

• normed type neighborhood lemmas

  enhancement ✨
  #2030·amolinamounier opened Jul 15, 2026Collaborator·

  ·

  · 1.19.0
  5

• Lemmas for functions bounded on a range

  #2028·amolinamounier opened Jul 15, 2026Collaborator·

  ·

  · 1.19.0

• Hausdorff ctvs

  #2022·mkerjean opened Jul 8, 2026Collaborator·

  ·

• Measurable type for normed modules (generalizes PR#2016)

  enhancement ✨
  #2017·Brixfoly opened Jul 7, 2026Contributor·

  ·

  · 1.19.0
  6

• Topology lemmas

  #2014·Brixfoly opened Jul 1, 2026Contributor·

  ·
  6

• Initial topology induced by a family of functions

  #2003·mkerjean opened Jun 21, 2026Collaborator·

  ·
  4