Code

monotonous and derivative#1448

Code

Merged

affeldt-aist merged 8 commits intomath-comp:mastermath-comp/analysis:masterfrom affeldt-aist:derive_20250107affeldt-aist/analysis:derive_20250107Copy head branch name to clipboardFeb 4, 2025

+339-18

Commits

Commits on Feb 4, 2025

• monotonous and derivative

  Show description for ce6c2f6
  

  affeldt-aist

  and

  IshiguroYoshihiro

  committed
  ce6c2f6

  Copy full SHA for ce6c2f6

• more lemmas

  Show description for f67c041
  

  affeldt-aist

  and

  IshiguroYoshihiro

  committed
  f67c041

  Copy full SHA for f67c041

• add interiorT, decr/incr_derive1_le0/ge0(_itv, _itvy, itvNy)

  

  IshiguroYoshihiro

  authored and

  affeldt-aist

  committed
  ed28e96

  Copy full SHA for ed28e96

• generalize interior_itv

  

  IshiguroYoshihiro

  authored and

  affeldt-aist

  committed
  0fe62b7

  Copy full SHA for 0fe62b7

• add interior_id and closureT

  

  t6s

  authored and

  affeldt-aist

  committed
  99df4a5

  Copy full SHA for 99df4a5

• move intriorI back

  

  t6s

  authored and

  affeldt-aist

  committed
  f56977e

  Copy full SHA for f56977e

• fix

  affeldt-aist

  committed
  742135e

  Copy full SHA for 742135e

• rename ge0r to ger0

  

  t6s

  authored and

  affeldt-aist

  committed
  b5dfe47

  Copy full SHA for b5dfe47