Notably, `NormedSpace.to_uniformContinuousConstSMul` is generalized to `BoundedSMul` on `PseudoMetricSpace`s, relaxing the scalar considerably from normed fields.



Co-authored-by: Eric Wieser <efw@google.com>

Delete `Algebra.Bounds` and `Algebra.Order.Pointwise`. Create
* `Algebra.Order.Field.Pointwise` for lemmas about pointwise operations in linear ordered fields
* `Algebra.Order.Group.CompleteLattice` for distributivity of group operations over supremum/infimum
* `Algebra.Order.Group.Pointwise.Bounds` for boundedness of pointwise-defined sets
* `Algebra.Order.Group.Pointwise.CompleteLattice` for lemmas about the supremum/infimum of pointwise-defined sets.

…identity (#17065)

In a closed monoidal category, the internal hom defined by mapping out of the monoidal unit is naturally isomorphic to the identity. This specializes to an analogous result about exponentiating with the terminal object in a cartesian closed category.

Co-authored-by: [Dagur Asgeirsson](https://github.com/dagurtomas)

This PR adds two lemmas about monotonicity for `lfpApprox` and `gfpApprox` each. I found them helpful when working with the API.



Co-authored-by: Ira Fesefeldt <public@feuervogel.me>
Co-authored-by: Ira Fesefeldt <9974411+PhoenixIra@users.noreply.github.com>

This adds the [Woodbury Identity](https://en.wikipedia.org/wiki/Woodbury_matrix_identity).

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Woodbury.20identity/near/462245284)

Also corrects some bad deprecations introduced in #16590, which affected development of this PR.

Co-authored-by: Mohanad Ahmad



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…17111)

… to `AnalyticOn` (#17146)

For coherence with `ContinuousOn`, `DifferentiableOn` and so on. See Zulip https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/Integrate.20analytic.20functions.20in.20the.20smooth.20hierarchy/near/471899268

This is 90% renaming all `AnalyticOn` to `AnalyticOnNhd` and then `AnalyticWithinOn` to `AnalyticOn`, and then adding deprecations. The 10% remaining is, when adding a deprecation `alias AnalyticOn.foo := AnalyticOnNhd.foo`, I noticed that `AnalyticOn.foo` would definitely make sense (with the new meaning of `AnalyticOn`), so I added the lemma with the new meaning instead of deprecating the old one.