Repository navigation

feat: use `IsApply` for `ContinuousMap` - #45093

Open

EtienneC30 wants to merge 37 commits into

leanprover-community:masterfrom

EtienneC30:apply-continuous

Open

feat: use `IsApply` for `ContinuousMap`#45093
EtienneC30 wants to merge 37 commits into
leanprover-community:masterfrom
EtienneC30:apply-continuous

Commits on Oct 20, 2026
- feat: use `IsApply` for `SimpleFunc`
  EtienneC30
  committed
  1deed06
- fix
  EtienneC30
  committed
  b1fd5d6
- fix
  EtienneC30
  committed
  a8f432b
- fix
  EtienneC30
  committed
  4baf5c9
- fix
  EtienneC30
  committed
  751a37f
- use where and fast_instance%
  EtienneC30
  committed
  2c518b4
- feat: use `IsApply` for `BoundedContinuousFunction`
  EtienneC30
  committed
  6b2377a
- protect deprecated lemmas
  EtienneC30
  committed
  76a7f52
- make deprecations protected
  EtienneC30
  committed
  2090445
- Merge branch 'apply-simple-func' into apply-bcf
  EtienneC30
  committed
  9805c65
- fix
  EtienneC30
  committed
  10442cd
- fix
  EtienneC30
  committed
  4bc1e07
- fix
  EtienneC30
  committed
  0db37db
- wip
  EtienneC30
  committed
  ece8a4a
- add deleted nsmul decls
  EtienneC30
  committed
  3186166
- Merge branch 'apply-bcf' into apply-continuous
  EtienneC30
  committed
  907166d
- wip
  EtienneC30
  committed
  224c0f6
- deprecate zpow lemmas
  EtienneC30
  committed
  2bee4df
- feat: use `IsApply` for `ContinuousMap`
  EtienneC30
  committed
  f592db1
- Merge branch 'apply-simple-func' into apply-bcf
  EtienneC30
  committed
  0fbf6ca
- Merge branch 'apply-bcf' into apply-continuous
  EtienneC30
  committed
  7d43292
- fix
  EtienneC30
  committed
  47ba4f4
- fix
  EtienneC30
  committed
  c3c0fe6
Commits on Oct 21, 2026
- Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into apply-bcf
  EtienneC30
  committed
  7ecf5af
- Merge branch 'apply-bcf' into apply-continuous
  EtienneC30
  committed
  2440c96
- remove useless todo
  EtienneC30
  committed
  94c50ec
- wip
  EtienneC30
  committed
  e412e87
- make smul_apply protected
  EtienneC30
  committed
  be08250
- fix
  EtienneC30
  committed
  22f0b4d
- Merge branch 'apply-bcf' into apply-finmeas
  EtienneC30
  committed
  3b6769b
- feat: use `IsApply` for `FiniteMeasure`
  EtienneC30
  committed
  14ffdaa
- Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into apply-finmeas
  EtienneC30
  committed
  f6fef85
- Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into apply-continuous
  EtienneC30
  committed
  5a20da4
- Merge branch 'apply-finmeas' into apply-continuous
  EtienneC30
  committed
  01efa0d
- Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into apply-continuous
  EtienneC30
  committed
  cb65f8e
Commits on Oct 23, 2026
- unsqueeze simps
  EtienneC30
  committed
  5a2f5ba
Commits on Oct 28, 2026
- Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into apply-continuous
  EtienneC30
  committed
  a81cdf6

Commits

Commits on Oct 20, 2026

Commits on Oct 21, 2026

Commits on Oct 23, 2026

Commits on Oct 28, 2026