Code

feat: generalize normal functions#20504

Code

Open

vihdzp wants to merge 13 commits intomasterleanprover-community/mathlib4:masterfrom vi.normalleanprover-community/mathlib4:vi.normalCopy head branch name to clipboard

+223-12

Commits

Commits on Jan 5, 2025

• start

  vihdzp

  committed
  54536e4

• prove

  vihdzp

  committed
  163fc26

Commits on Jan 6, 2025

• progress

  vihdzp

  committed
  c604092

• Merge branch 'vi.isLUB_Iio' into vi.normal

  vihdzp

  committed
  636ce89

• deprs + tweaks

  vihdzp

  committed
  f4b79ed

• generalize

  vihdzp

  committed
  cef1b6c

• progress

  vihdzp

  committed
  1a519ef

• add other aux lemma

  vihdzp

  committed
  3c69b33

• Merge branch 'vi.limitLemmas' into vi.normal

  vihdzp

  committed
  716f63f

• normal functions!

  vihdzp

  committed
  4f26b50

• fix

  vihdzp

  committed
  1db7883

• Merge branch 'vi.limitLemmas' into vi.normal

  vihdzp

  committed
  1ef7782

• namespace

  vihdzp

  committed
  fd1844f