Skip to content

[Merged by Bors] - chore: Rename ClosedEmbedding to IsClosedEmbedding#17937

Closed
YaelDillies wants to merge 5 commits intomasterfrom
rename_closed_embedding
Closed

[Merged by Bors] - chore: Rename ClosedEmbedding to IsClosedEmbedding#17937
YaelDillies wants to merge 5 commits intomasterfrom
rename_closed_embedding

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Oct 19, 2024 •
edited
Loading

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 ClosedEmbedding is)
  2. namespacing it inside Topology

Zulip. See #15993 for context.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-topology Topological spaces, uniform spaces, metric spaces, filters labels Oct 19, 2024
@YaelDillies YaelDillies mentioned this pull request Oct 19, 2024
Closed
11 tasks
@github-actions
Copy link
Copy Markdown

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

PR summary da9f95e67a

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ ArzelaAscoli.compactSpace_of_isClosedEmbedding
+ ArzelaAscoli.isCompact_closure_of_isClosedEmbedding
+ Continuous.isClosedEmbedding
+ Function.LeftInverse.isClosedEmbedding
+ Int.isClosedEmbedding_coe_rat
+ IsClosed.isClosedEmbedding_subtypeVal
+ IsClosed.isProperMap_subtypeVal
+ IsClosedEmbedding
+ IsClosedEmbedding.LindelofSpace
+ IsClosedEmbedding.compactSpace
+ IsClosedEmbedding.isCompact_preimage
+ IsClosedEmbedding.isLindelof_preimage
+ IsClosedEmbedding.isProperMap
+ IsClosedEmbedding.locallyCompactSpace
+ IsClosedEmbedding.measurable
+ IsClosedEmbedding.measurableEmbedding
+ IsClosedEmbedding.nonLindelofSpace
+ IsClosedEmbedding.noncompactSpace
+ IsClosedEmbedding.normalSpace
+ IsClosedEmbedding.paracompactSpace
+ IsClosedEmbedding.quasiSober
+ IsClosedEmbedding.restrictPreimage
+ IsClosedEmbedding.sigmaCompactSpace
+ IsClosedEmbedding.subtypeVal
+ IsClosedEmbedding.t4Space
+ IsClosedEmbedding.tendsto_coLindelof
+ IsClosedEmbedding.tendsto_cocompact
+ IsClosedEmbedding.topologicalKrullDim_le
+ IsClosedEmbedding.weaklyLocallyCompactSpace
+ IsProperMap.restrict
+ IsUniformEmbedding.toIsClosedEmbedding
+ LinearMap.isClosedEmbedding_of_injective
+ Nat.isClosedEmbedding_coe_rat
+ Set.restrictPreimage_isClosedEmbedding
+ ULift.isClosedEmbedding_down
+ UniformEmbedding.toIsClosedEmbedding
+ _root_.IsClosedEmbedding.integral_map
+ _root_.IsClosedEmbedding.of_continuous_injective_isClosedMap
+ _root_.IsClosedEmbedding.of_embedding_closed
+ _root_.IsClosedEmbedding.polishSpace
+ _root_.IsClosedEmbedding.setIntegral_map
+ _root_.IsClosedEmbedding.set_integral_map
+ _root_.isClosedEmbedding_id
+ autEmbedding_isClosedEmbedding
+ cfcHom_isClosedEmbedding
+ cfcₙHom_isClosedEmbedding
+ comp_isClosedEmbedding
+ exists_extension_forall_exists_le_ge_of_isClosedEmbedding
+ exists_extension_forall_mem_Icc_of_isClosedEmbedding
+ exists_extension_norm_eq_of_isClosedEmbedding
+ exists_extension_norm_eq_of_isClosedEmbedding'
+ exists_extension_of_isClosedEmbedding
+ instance : (topologically IsClosedEmbedding).RespectsIso
+ instance : CompactSpace (Aut F) := IsClosedEmbedding.compactSpace (autEmbedding_isClosedEmbedding F)
+ instance : MetrizableSpace (OnePoint ℕ) := isClosedEmbedding_natUnionInftyEmbedding.metrizableSpace
+ instance : NoncompactSpace ℚ := Int.isClosedEmbedding_coe_rat.noncompactSpace
+ instance : NoncompactSpace ℝ := Int.isClosedEmbedding_coe_real.noncompactSpace
+ isClosedEmbedding_cfcAux
+ isClosedEmbedding_cfcₙAux
+ isClosedEmbedding_cfcₙHom_of_cfcHom
+ isClosedEmbedding_coe
+ isClosedEmbedding_coe_ennreal
+ isClosedEmbedding_comap_of_surjective
+ isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top
+ isClosedEmbedding_inclusion
+ isClosedEmbedding_inl
+ isClosedEmbedding_inr
+ isClosedEmbedding_isLocalAtTarget
+ isClosedEmbedding_mk
+ isClosedEmbedding_mk_symm
+ isClosedEmbedding_natUnionInftyEmbedding
+ isClosedEmbedding_nonUnitalStarAlgHom
+ isClosedEmbedding_of_pairwise_le_dist
+ isClosedEmbedding_of_spaced_out
+ isClosedEmbedding_sigmaMk
+ isClosedEmbedding_smul_left
+ isClosedEmbedding_starAlgHom
+ isClosedEmbedding_toContinuousMultilinearMap
+ isClosedEmbedding_update
+ isSeparatedMap_iff_isClosedEmbedding
+ properSMul_of_isClosedEmbedding
+ totalSpaceMk_isClosedEmbedding
++ exists_extension_forall_mem_of_isClosedEmbedding
++ isClosedEmbedding_coe_real
++ isClosedEmbedding_toContinuousMap
+++++++ isClosedEmbedding
+++++++------- closedEmbedding
++-- closedEmbedding_coe_real
++-- closedEmbedding_toContinuousMap
++-- exists_extension_forall_mem_of_closedEmbedding
- closedEmbedding_isLocalAtTarget
- instance : (topologically ClosedEmbedding).RespectsIso
- instance : CompactSpace (Aut F) := ClosedEmbedding.compactSpace (autEmbedding_closedEmbedding F)
- instance : MetrizableSpace (OnePoint ℕ) := closedEmbedding_natUnionInftyEmbedding.metrizableSpace
- instance : NoncompactSpace ℚ := Int.closedEmbedding_coe_rat.noncompactSpace
- instance : NoncompactSpace ℝ := Int.closedEmbedding_coe_real.noncompactSpace

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.

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Oct 20, 2024
@YaelDillies
chore: Rename ClosedEmbedding to IsClosedEmbedding
299ac3b 
`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 neighborhing declarations (which `ClosedEmbedding` is)
2. namespacing it inside `Topology`

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rename.20.60Inducing.60.20and.20.60Embedding.60.3F). See #15993 for context.
@YaelDillies YaelDillies force-pushed the rename_closed_embedding branch from ecf97a4 to 299ac3b Compare October 20, 2024 08:04
@urkud
Copy link
Copy Markdown
Member

urkud commented Oct 20, 2024

Thanks! 🎉
bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 20, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 20, 2024
@YaelDillies
chore: Rename ClosedEmbedding to IsClosedEmbedding (#17937)
0dedd92 
`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 neighborhing declarations (which `ClosedEmbedding` is)
2. namespacing it inside `Topology`

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rename.20.60Inducing.60.20and.20.60Embedding.60.3F). See #15993 for context.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 20, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Rename ClosedEmbedding to IsClosedEmbedding [Merged by Bors] - chore: Rename ClosedEmbedding to IsClosedEmbedding Oct 20, 2024
@mathlib-bors mathlib-bors bot closed this Oct 20, 2024
@mathlib-bors mathlib-bors bot deleted the rename_closed_embedding branch October 20, 2024 13:50
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

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.

2 participants

@YaelDillies @urkud