feat(Condensed): light condensed objects #9515
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
This was referenced Jan 7, 2024
leanprover-community-mathlib4-bot
added
merge-conflict
leanprover-community-mathlib4-bot
added
the
merge-conflict
and a few more lemmas. From LeanAPAP
I suspect I will need some of these for #10660
`ball` for "bounded forall" and `bex` for "bounded exists" are from experience very confusing abbreviations. This PR renames them to `forall_mem` and `exists_mem` in the few `Set` lemma names that mention them. Also deprecate `ball_image_of_ball`, `mem_image_elim`, `mem_image_elim_on` since those lemmas are duplicates of the renamed lemmas (apart from argument order and implicitness, which I am also fixing by making the binder in the RHS of `forall_mem_image` semi-implicit), have obscure names and are completely unused.
Classifies by adding issue number #11215 to porting notes claiming "TODO".
Classifies by adding issue number #10756 to porting notes claiming anything semantically equivalent to: - "new lemma" - "added lemma"
From the sphere eversion project. In passing, we rename variables in one more lemma and use fun_prop in a tiny way.
…es of `PiTensorProduct` (#11152) * Prove some properties of `PiTensorProduct.map`, for example the compatibility with composition and reindeixing, and the fact that it sends the identity to the identity. * Construct `PiTensorProduct.map` as a `MultilinearMap` on the family of linear maps. * Upgrade `PiTensorProduct.map f` to a linear equivalence called `PiTensorProduct.congr f` when `f` is a family of linear equivalences. * For `ι` a `Fintype`, define the canonical linear equivalence (given by multiplication) `constantBaseRingEquiv` from `⨂ i : ι, R` and `R`. Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Introduces a new class, `PerfectSpace`, which requires that `Set.univ` is a perfect set. This is equivalent to say that no points are isolated (`perfectSpace_iff_forall_not_isolated`).
…e essentially surjective (#11239) Show that if `F.obj` is surjective, `F` is essentially surjective.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
This PR accompanies #11246, squeezing some non-terminal `simp`s highlighted by the linter until I decided to stop!
Classifies by adding issue number #11224 to porting notes claiming: > change `rw` to `erw`
Classifies by adding issue number #11227 to porting notes claiming anything equivalent to: - "added `dsimp`" - "`dsimp` added" - "`dsimp` now needed"
Classifies by adding issue number #11229 to porting notes claiming: > deprecated
Add `tendsto_of_integral_tendsto_of_monotone`, as well as `...of_antitone` and the corresponding results for `lintegral`. Also: - move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue. - add `lintegral_iInf'`, a version of `lintegral_iInf` for a.e.-measurable functions. We already have the corresponding `lintegral_iSup'`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…6262) This PR removes the default values for `nsmul` and `zsmul`, forcing the user to populate them manually. The previous behavior can be obtained by writing `nsmul := nsmulRec` and `zsmul := zsmulRec`, which is now in the docstring for these fields. The motivation here is to make it more obvious when module diamonds are being introduced, or at least where they might be hiding; you can now simply search for `nsmulRec` in the source code. Arguably we should do the same thing for `intCast`, `natCast`, `pow`, and `zpow` too, but diamonds are less common in those fields, so I'll leave them to a subsequent PR. Co-authored-by: Matthew Ballard <matt@mrb.email>
Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.
This adds instances of the continuous functional calculus for unital C⋆-algebras for normal, selfadjoint, and positive elements.
Makes the proof of this lemma shorter and perhaps cleaner by adding a new lemma and moving it forward to take advantage of the preexisting `card_eq_three` Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Some small changes to adapt to the 2024-03-16 nightly that can land in advance.
#11493) - Add `FreeGroup.closure_range_of`: the subgroup closure of the range of `FreeGroup.of : α → FreeGroup α` is `⊤`. (That is, the generators of a free group generate the free group.) - Add `PresentedGroup.closure_range_of`: the subgroup closure of the range of `PresentedGroup.of : α → PresentedGroup rels` is `⊤`. (That is, the generators of a presented group generate the presented group.)
Removes the `insertNth` section of this long file to its own new file. This section seems to be completely independent of the rest of the file, so this is a fairly easy split to make.
Classifies by adding issue number #10618 to porting notes claiming "`simp` can prove it".
This will become an error in 2024-03-16 nightly, possibly not permanently. Co-authored-by: Scott Morrison <scott@tqft.net>
…asic lemmas (#11561) Move lemmas to put similar ones together, replace `refine'` by `refine` and `=>` by `↦`. Lemmas added: * `singularPart_add_rnDeriv` and `rnDeriv_add_singularPart`: almost aliases of `haveLebesgueDecomposition_add` * `haveLebesgueDecomposition_smul'`, `haveLebesgueDecomposition_rnDeriv` * `singularPart_eq_zero_of_ac`, `singularPart_eq_zero`, `singularPart_self`, `singularPart_eq_self` Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Summability of `n ↦ 1 / |n + a| ^ s` and `n ↦ n ^ k exp (-r * n)`
.. in `equivOfPiLEquivPi`, `coePiBasisFun.toMatrix_eq_transpose`, `vecMul_surjective_iff_exists_left_inverse`, and `mulVec_surjective_iff_exists_right_inverse`
Adds a congruence lemma for `BEq` instances that makes use of `LawfulBEq` instances, and gives `congr!` the ability to use this congruence lemma. This is meant to help with diamonds that arise from interactions between Decidable and BEq instances.
This feature can be turned off using the `beqEq` configuration setting, like `congr! (config := { beqEq := false })`.
Currently you need to run ``` lake build ProofWidgets make tests ``` to reliably get tests to work. --- <!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Co-authored-by: Author Name <author@email.com> Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer/)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
|
Sorry, messed up when trying to merge another branch into this |
](https://gitpod.io/from-referrer/){kind=link}
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
New foundations for analytic geometry based on light condensed sets are being developed by Clausen-Scholze (see this youtube playlist).
This PR defines light condensed objects.
PreregularandFinitaryPreExtensiveimpliesPrecoherent#8643