Skip to content

[Merged by Bors] - feat: is{Inducing,Embedding}_prodMkLeft#25705

Closed
grunweg wants to merge 3 commits intomasterfrom
MR-embedding-prodMkLeft
Closed

[Merged by Bors] - feat: is{Inducing,Embedding}_prodMkLeft#25705
grunweg wants to merge 3 commits intomasterfrom
MR-embedding-prodMkLeft

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Jun 11, 2025 •
edited
Loading

Analoguous to isEmbedding_prodMk, which I've renamed to isEmbedding_prodMkRight for clarify.
Add isInducing_prodMk{Left,Right} also.

Open in Gitpod

@grunweg grunweg requested a review from YaelDillies June 11, 2025 16:03
@grunweg grunweg added easy < 20s of review time. See the lifecycle page for guidelines. t-topology Topological spaces, uniform spaces, metric spaces, filters labels Jun 11, 2025
@grunweg grunweg mentioned this pull request Jun 11, 2025
Closed
4 tasks
@grunweg grunweg marked this pull request as ready for review June 11, 2025 16:03
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 11, 2025 •
edited
Loading

PR summary 658f45e58d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ isEmbedding_prodMkLeft
+ isEmbedding_prodMkRight
+ isInducing_prodMkLeft
+ isInducing_prodMkRight

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

YaelDillies
YaelDillies approved these changes Jun 11, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you want a deprecated alias? Are there similar lemmas for other topological properties?

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 11, 2025

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 11, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jun 11, 2025

Thanks! I added the deprecation (not sure how I missed that) and analogous lemmas for inducing maps.
In that file, there are no further unmatched theorems for left which are missing for right, and apparently no other results for Prod.mk.

@grunweg grunweg changed the title feat: isEmbedding_prodMkLeft feat: is{Inducing,Embedding}_prodMkLeft Jun 11, 2025
jcommelin
jcommelin reviewed Jun 12, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jun 12, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jun 12, 2025
@grunweg
feat: is{Inducing,Embedding}_prodMkLeft (#25705)
789aae7 
Analoguous to `isEmbedding_prodMk`, which I've renamed to `isEmbedding_prodMkRight` for clarify.
Add `isInducing_prodMk{Left,Right}` also.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 12, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: is{Inducing,Embedding}_prodMkLeft [Merged by Bors] - feat: is{Inducing,Embedding}_prodMkLeft Jun 12, 2025
@mathlib-bors mathlib-bors bot closed this Jun 12, 2025
@mathlib-bors mathlib-bors bot deleted the MR-embedding-prodMkLeft branch June 12, 2025 06:02
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jun 12, 2025

Thank you for the fast review, these are great!

vlad902 added a commit to vlad902/mathlib4 that referenced this pull request Jun 12, 2025
@vlad902
Merge branch 'master' into vlad.tsyrklevich/cg4-istree
7f5ce20 
* master: (447 commits)
  chore(Data/Set): move very basic lemmas earlier (leanprover-community#25707)
  feat: preserve draft status when migrating PRs to fork (leanprover-community#25777)
  chore(Data/Set/Basic): deprecate lemmas that abuse the `Set α := α → Prop` defeq (leanprover-community#25669)
  refactor: redefine `ProperCone` as an `abbrev` for `ClosedSubmodule` (leanprover-community#25204)
  feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm (leanprover-community#25564)
  fix: outdated docstring (leanprover-community#25717)
  feat(MeasureTheory): convolution of measures with densities  (leanprover-community#25718)
  feat: make sure that the simp normal form of equiv-like classes pushes `symm` and `trans` to the right (leanprover-community#25604)
  feat(ModelTheory): Formula.iSup and iInf (leanprover-community#21948)
  feat(RingTheory/Polynomial/ContentIdeal): the content ideal of a polynomial. (leanprover-community#25333)
  fix: typo in labels_from_comment.yml (leanprover-community#25727)
  feat: is{Inducing,Embedding}_prodMkLeft (leanprover-community#25705)
  feat: check that the mathlib options exist (leanprover-community#25687)
  feat(Algebra/Group/Even): Add missing lemmas (leanprover-community#20818)
  refactor: make `Matrix.kroneckerTMulAlgEquiv` heterogeneous (leanprover-community#25693)
  feat: allow contributors to remove labels with comments (leanprover-community#25723)
  chore: disable build.yml and bors.yml on forks (leanprover-community#25722)
  feat: improvements to user_activity_report.py (leanprover-community#25721)
  chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701)
  chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701)
  ...
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025
@grunweg
feat: is{Inducing,Embedding}_prodMkLeft (leanprover-community#25705)
0d44a02 
Analoguous to `isEmbedding_prodMk`, which I've renamed to `isEmbedding_prodMkRight` for clarify.
Add `isInducing_prodMk{Left,Right}` also.
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025
@grunweg
feat: is{Inducing,Embedding}_prodMkLeft (leanprover-community#25705)
6ce4ea8 
Analoguous to `isEmbedding_prodMk`, which I've renamed to `isEmbedding_prodMkRight` for clarify.
Add `isInducing_prodMk{Left,Right}` also.
@grunweg grunweg mentioned this pull request Jun 18, 2025
Open
4 tasks
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@grunweg @callesonne
feat: is{Inducing,Embedding}_prodMkLeft (leanprover-community#25705)
4e798bb 
Analoguous to `isEmbedding_prodMk`, which I've renamed to `isEmbedding_prodMkRight` for clarify.
Add `isInducing_prodMk{Left,Right}` also.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@grunweg @jcommelin @YaelDillies