-
Notifications
You must be signed in to change notification settings - Fork 324
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
sync to master #17157
sync to master #17157
Conversation
This PR updates the Mathlib dependencies.
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>
… 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.
a1a093f
into
yoh-tanimoto-innerproductspace-quotient
PR summary 5d4532a2ddImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
No description provided.