Skip to content

[Merged by Bors] - chore: Rename Inducing to IsInducing#18330

Closed
YaelDillies wants to merge 6 commits intomasterfrom
rename_inducing
Closed

[Merged by Bors] - chore: Rename Inducing to IsInducing#18330
YaelDillies wants to merge 6 commits intomasterfrom
rename_inducing

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Oct 28, 2024

Function.Embedding is a type while Embedding is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards

  1. renaming Embedding to IsEmbedding and similarly for neighboring declarations (which Inducing is)
  2. namespacing it inside Topology

Open in Gitpod

@YaelDillies YaelDillies added WIP Work in progress t-topology Topological spaces, uniform spaces, metric spaces, filters labels Oct 28, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 28, 2024 •
edited
Loading

PR summary 1130c25000

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ EquicontinuousOn.isInducing_uniformOnFun_iff_pi
+ FiberBundle.Prod.isInducing_diag
+ IsEmbedding.isSeparable_preimage
+ IsInducing
+ IsInducing.alexandrovDiscrete
+ IsInducing.codRestrict
+ IsInducing.comapPseudoMetricSpace
+ IsInducing.comp
+ IsInducing.continuousConstSMul
+ IsInducing.continuousInv
+ IsInducing.continuousMul
+ IsInducing.continuousOn_iff
+ IsInducing.continuousSMul
+ IsInducing.continuousWithinAt_iff
+ IsInducing.frechetUrysohnSpace
+ IsInducing.generalizingMap
+ IsInducing.hasProd_iff
+ IsInducing.id
+ IsInducing.induced
+ IsInducing.injective
+ IsInducing.inseparable_iff
+ IsInducing.isClosedMap
+ IsInducing.isCompact_iff
+ IsInducing.isCompact_preimage
+ IsInducing.isCompact_preimage'
+ IsInducing.isCompact_preimage_iff
+ IsInducing.isEmbedding
+ IsInducing.isLindelof_iff
+ IsInducing.isLindelof_preimage
+ IsInducing.isLocallyClosed_iff
+ IsInducing.isOpenMap
+ IsInducing.isPathConnected_iff
+ IsInducing.isPreconnected_image
+ IsInducing.isSeparable_preimage
+ IsInducing.isSigmaCompact_iff
+ IsInducing.joinedIn_image
+ IsInducing.locallyCompactSpace
+ IsInducing.multipliable_iff_tprod_comp_mem_range
+ IsInducing.of_codRestrict
+ IsInducing.of_comp
+ IsInducing.of_comp_iff
+ IsInducing.prodMap
+ IsInducing.r0Space
+ IsInducing.r1Space
+ IsInducing.regularSpace
+ IsInducing.restrictPreimage
+ IsInducing.secondCountableTopology
+ IsInducing.specializes_iff
+ IsInducing.specializingMap
+ IsInducing.subtypeVal
+ IsInducing.topologicalGroup
+ IsInducing.withSeminorms
+ IsOpenEmbedding.isInducing
+ IsTopologicalBasis.isInducing
+ IsUniformInducing.isInducing
+ Set.restrictPreimage_isInducing
+ UniformInducing.isInducing
+ _root_.IsInducing.firstCountableTopology
+ _root_.IsInducing.noetherianSpace
+ _root_.IsInducing.pseudoMetrizableSpace
+ comap_isInducing_of_surjective
+ exists_isInducing_l_infty
+ induced
+ instance : ContinuousMul αˣ := isInducing_embedProduct.continuousMul (embedProduct α)
+ instance : ContinuousNeg (ball (0 : E) r) := IsInducing.subtypeVal.continuousNeg fun _ => rfl
+ instance : ContinuousNeg (closedBall (0 : E) r) := IsInducing.subtypeVal.continuousNeg fun _ => rfl
+ instance : ContinuousNeg (sphere (0 : E) r) := IsInducing.subtypeVal.continuousNeg fun _ => rfl
+ instance {p : X → Prop} : R0Space {x // p x} := IsInducing.subtypeVal.r0Space
+ isEmbedding_iff_isInducing
+ isInducing_coeFn
+ isInducing_const_prod
+ isInducing_embedProduct
+ isInducing_iff_nhds
+ isInducing_mk_symm
+ isInducing_nhds
+ isInducing_postcomp
+ isInducing_prodMap
+ isInducing_prod_const
+ isInducing_pullback_to_prod
+ isInducing_sigmaMap
+ isInducing_toContinuousMap
+ isInducing_toProd
+ localization_comap_isInducing
+ productOfMemOpens_isInducing
+ toHomeomorphOfIsInducing
+ totalSpaceMk_isInducing
++ isInducing_mk
+++++ isInducing
++++--- inducing
++-- inducing_mk
+-+- continuous
- _root_.IsEmbedding.isSeparable_preimage
- instance : ContinuousMul αˣ
- instance : ContinuousNeg (ball (0 : E) r)
- instance : ContinuousNeg (closedBall (0 : E) r)
- instance : ContinuousNeg (sphere (0 : E) r)
- instance {p : X → Prop} : R0Space {x // p x} := inducing_subtype_val.r0Space

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.

@YaelDillies YaelDillies mentioned this pull request Oct 28, 2024
Closed
11 tasks
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 28, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 28, 2024
@YaelDillies YaelDillies force-pushed the rename_inducing branch 2 times, most recently from e5cb1de to d455e51 Compare October 28, 2024 22:31
@YaelDillies YaelDillies mentioned this pull request Oct 28, 2024
Closed
@YaelDillies YaelDillies added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress labels Oct 28, 2024
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Oct 29, 2024

Thanks for doing this

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2024

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 29, 2024
@YaelDillies YaelDillies added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Oct 29, 2024
@ghost
Copy link
Copy Markdown

ghost commented Oct 29, 2024

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Oct 29, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 29, 2024
@YaelDillies
chore: Rename Inducing to IsInducing (#18330)
33d49bb 
`Function.Embedding` is a type while `Embedding` is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards
1. renaming `Embedding` to `IsEmbedding` and similarly for neighboring declarations (which `Inducing` is)
2. namespacing it inside `Topology`
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Rename Inducing to IsInducing [Merged by Bors] - chore: Rename Inducing to IsInducing Oct 29, 2024
@mathlib-bors mathlib-bors bot closed this Oct 29, 2024
@mathlib-bors mathlib-bors bot deleted the rename_inducing branch October 29, 2024 15:17
jcommelin pushed a commit that referenced this pull request Oct 29, 2024
@YaelDillies @jcommelin
chore: Rename Inducing to IsInducing (#18330)
d337087 
`Function.Embedding` is a type while `Embedding` is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards
1. renaming `Embedding` to `IsEmbedding` and similarly for neighboring declarations (which `Inducing` is)
2. namespacing it inside `Topology`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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

@YaelDillies @jcommelin @leanprover-community-bot-assistant