Skip to content
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.

Sign up for GitHub

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

Jump to bottom

chore: rename NormalSpace to T4Space #6892

Closed
wants to merge 3 commits into from
Closed

chore: rename NormalSpace to T4Space #6892

wants to merge 3 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Aug 31, 2023

Open in Gitpod

@urkud urkud added awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters labels Aug 31, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Aug 31, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Aug 31, 2023
sgouezel
sgouezel reviewed Sep 2, 2023
View reviewed changes
Mathlib/Topology/Separation.lean
@@ -1734,21 +1734,21 @@ end T3

section Normality

-- todo: rename this to `T4Space`, introduce `NormalSpace` without `T1Space` assumption
-- todo: rename this to `T4Space`, introduce `T4Space` without `T1Space` assumption
Copy link
Contributor

Choose a reason for hiding this comment

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

can you update the todo?

Mathlib/Topology/Separation.lean
/-- A T₄ space, also known as a normal space (although this condition sometimes
omits T₂), is one in which for every pair of disjoint closed sets `C` and `D`,
there exist disjoint open sets containing `C` and `D` respectively. -/
class NormalSpace (α : Type u) [TopologicalSpace α] extends T1Space α : Prop where
class T4Space (α : Type u) [TopologicalSpace α] extends T1Space α : Prop where
/-- Two disjoint sets in a normal space admit disjoint neighbourhoods. -/
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
/-- Two disjoint sets in a normal space admit disjoint neighbourhoods. -/
/-- Two disjoint closed sets in a T₄ space admit disjoint neighbourhoods. -/

Mathlib/Topology/Separation.lean
@@ -1800,7 +1800,7 @@ variable (α)

/-- A T₃ topological space with second countable topology is a normal space.
This lemma is not an instance to avoid a loop. -/
theorem normalSpaceOfT3SecondCountable [SecondCountableTopology α] [T3Space α] : NormalSpace α := by
theorem t4SpaceOfT3SecondCountable [SecondCountableTopology α] [T3Space α] : T4Space α := by
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
theorem t4SpaceOfT3SecondCountable [SecondCountableTopology α] [T3Space α] : T4Space α := by
theorem t4Space_of_t3Space_secondCountable [SecondCountableTopology α] [T3Space α] : T4Space α := by

looks like the naming convention was not respected on this one.

Mathlib/Topology/UniformSpace/Compact.lean
@@ -104,7 +104,7 @@ def uniformSpaceOfCompactT2 [TopologicalSpace γ] [CompactSpace γ] [T2Space γ]
have diag_subset : diagonal γ ⊆ interior V := subset_interior_iff_mem_nhdsSet.2 V_in
have x_ne_y : x ≠ y := mt (@diag_subset (x, y)) this
-- Since γ is compact and Hausdorff, it is normal, hence T₃.
haveI : NormalSpace γ := normalOfCompactT2
haveI : T4Space γ := T4Space.of_compact_t2Space
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
haveI : T4Space γ := T4Space.of_compact_t2Space
have : T4Space γ := T4Space.of_compact_t2Space

Mathlib/Geometry/Manifold/Metrizable.lean
@@ -26,7 +26,7 @@ theorem ManifoldWithCorners.metrizableSpace {E : Type*} [NormedAddCommGroup E] [
(M : Type*) [TopologicalSpace M] [ChartedSpace H M] [SigmaCompactSpace M] [T2Space M] :
MetrizableSpace M := by
haveI := I.locallyCompactSpace; haveI := ChartedSpace.locallyCompactSpace H M
haveI : NormalSpace M := normal_of_paracompact_t2
haveI : T4Space M := .of_paracompact_t2Space
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
haveI : T4Space M := .of_paracompact_t2Space
have : T4Space M := .of_paracompact_t2Space

No need for haveI, here and below.

@ADedecker ADedecker added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 2, 2023
@urkud urkud mentioned this pull request Sep 10, 2023
Closed
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Sep 10, 2023
bors bot pushed a commit that referenced this pull request Sep 12, 2023
@urkud
refactor: split NormalSpace into NormalSpace and T4Space (#7072)
cc5af48 
* Rename `NormalSpace` to `T4Space`.
* Add `NormalSpace`, a version without the `T1Space` assumption.
* Adjust some theorems.
* Supersedes thus closes #6892.
* Add some instance cycles, see #2030
bors bot pushed a commit that referenced this pull request Sep 12, 2023
@urkud
refactor: split NormalSpace into NormalSpace and T4Space (#7072)
98e99da 
* Rename `NormalSpace` to `T4Space`.
* Add `NormalSpace`, a version without the `T1Space` assumption.
* Adjust some theorems.
* Supersedes thus closes #6892.
* Add some instance cycles, see #2030
bors bot pushed a commit that referenced this pull request Sep 12, 2023
@urkud
refactor: split NormalSpace into NormalSpace and T4Space (#7072)
c24a080 
* Rename `NormalSpace` to `T4Space`.
* Add `NormalSpace`, a version without the `T1Space` assumption.
* Adjust some theorems.
* Supersedes thus closes #6892.
* Add some instance cycles, see #2030
bors bot pushed a commit that referenced this pull request Sep 12, 2023
@urkud
refactor: split NormalSpace into NormalSpace and T4Space (#7072)
1f297aa 
* Rename `NormalSpace` to `T4Space`.
* Add `NormalSpace`, a version without the `T1Space` assumption.
* Adjust some theorems.
* Supersedes thus closes #6892.
* Add some instance cycles, see #2030
@bors bors bot closed this in bf815bd Sep 12, 2023
@urkud urkud deleted the YK-Normal-rename branch September 19, 2023 04:23
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@urkud @kodyvajjha
refactor: split NormalSpace into NormalSpace and T4Space (#7072)
7ab4b5d 
* Rename `NormalSpace` to `T4Space`.
* Add `NormalSpace`, a version without the `T1Space` assumption.
* Adjust some theorems.
* Supersedes thus closes #6892.
* Add some instance cycles, see #2030
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. 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.

None yet
4 participants
@urkud @sgouezel @ADedecker @leanprover-community-mathlib4-bot