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

[Merged by Bors] - chore: implement porting notes about Polish spaces #6991

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore: implement porting notes about Polish spaces #6991

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
08c725b
porting notes
Felix-Weilacher Sep 6, 2023
f6678cf
use extends
Felix-Weilacher Sep 7, 2023
e323610
remove comment
Felix-Weilacher Sep 8, 2023
7d50e4b
add docstring
Felix-Weilacher Sep 8, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
26 changes: 0 additions & 26 deletions Mathlib/MeasureTheory/Constructions/Polish.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -544,7 +544,6 @@ instance QuotientGroup.borelSpace {G : Type*} [TopologicalSpace G] [PolishSpace
[IsClosed (N : Set G)] : BorelSpace (G ⧸ N) :=
-- porting note: 1st and 3rd `haveI`s were not needed in Lean 3
haveI := Subgroup.t3_quotient_of_isClosed N
haveI := @PolishSpace.secondCountableTopology G
haveI := QuotientGroup.secondCountableTopology (Γ := N)
Quotient.borelSpace
#align quotient_group.borel_space QuotientGroup.borelSpace
Expand Down Expand Up @@ -845,28 +844,8 @@ end MeasureTheory

/-! ### The Borel Isomorphism Theorem -/

-- Porting note: Move to topology/metric_space/polish when porting.
instance (priority := 50) polish_of_countable [h : Countable α] [DiscreteTopology α] :
PolishSpace α := by
obtain ⟨f, hf⟩ := h.exists_injective_nat
have : ClosedEmbedding f := by
apply closedEmbedding_of_continuous_injective_closed continuous_of_discreteTopology hf
exact fun t _ => isClosed_discrete _
exact this.polishSpace
#align polish_of_countable polish_of_countable

namespace PolishSpace

/- Porting note: This is to avoid a loop in TC inference. When ported to Lean 4, this will not
be necessary, and `secondCountable_of_polish` should probably
just be added as an instance soon after the definition of `PolishSpace`.-/
private theorem secondCountable_of_polish [h : PolishSpace α] : SecondCountableTopology α :=
h.secondCountableTopology

attribute [-instance] polishSpace_of_complete_second_countable

attribute [local instance] secondCountable_of_polish

variable {β : Type*} [TopologicalSpace β] [PolishSpace α] [PolishSpace β]

variable [MeasurableSpace α] [MeasurableSpace β] [BorelSpace α] [BorelSpace β]
Expand Down Expand Up @@ -907,11 +886,6 @@ end PolishSpace

namespace MeasureTheory

-- Porting note: todo after the port: move to topology/metric_space/polish
instance instPolishSpaceUniv [PolishSpace α] : PolishSpace (univ : Set α) :=
isClosed_univ.polishSpace
#align measure_theory.set.univ.polish_space MeasureTheory.instPolishSpaceUniv

variable (α)
variable [MeasurableSpace α] [PolishSpace α] [BorelSpace α]

Expand Down
31 changes: 20 additions & 11 deletions Mathlib/Topology/MetricSpace/Polish.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,8 +62,8 @@ other way around as this is the most common use case.

To endow a Polish space with a complete metric space structure, do `letI := upgradePolishSpace α`.
-/
class PolishSpace (α : Type*) [h : TopologicalSpace α] : Prop where
secondCountableTopology : SecondCountableTopology α
class PolishSpace (α : Type*) [h : TopologicalSpace α]
extends SecondCountableTopology α : Prop where
complete : ∃ m : MetricSpace α, m.toUniformSpace.toTopologicalSpace = h ∧
@CompleteSpace α m.toUniformSpace
#align polish_space PolishSpace
Expand All @@ -76,8 +76,7 @@ class UpgradedPolishSpace (α : Type*) extends MetricSpace α, SecondCountableTo
#align upgraded_polish_space UpgradedPolishSpace

instance (priority := 100) polishSpace_of_complete_second_countable [m : MetricSpace α]
[h : SecondCountableTopology α] [h' : CompleteSpace α] : PolishSpace α where
secondCountableTopology := h
[SecondCountableTopology α] [h' : CompleteSpace α] : PolishSpace α where
complete := ⟨m, rfl, h'⟩
#align polish_space_of_complete_second_countable polishSpace_of_complete_second_countable

Expand All @@ -97,7 +96,7 @@ theorem complete_polishSpaceMetric (α : Type*) [ht : TopologicalSpace α] [h :
def upgradePolishSpace (α : Type*) [TopologicalSpace α] [PolishSpace α] :
UpgradedPolishSpace α :=
letI := polishSpaceMetric α
{ complete_polishSpaceMetric α, PolishSpace.secondCountableTopology with }
{ complete_polishSpaceMetric α with }
#align upgrade_polish_space upgradePolishSpace

namespace PolishSpace
Expand All @@ -117,11 +116,6 @@ instance pi_countable {ι : Type*} [Countable ι] {E : ι → Type*} [∀ i, Top
infer_instance
#align polish_space.pi_countable PolishSpace.pi_countable

/-- Without this instance, Lean 3 was unable to find `PolishSpace (ℕ → ℕ)` by typeclass inference.
Porting note: TODO: test with Lean 4. -/
instance nat_fun [TopologicalSpace α] [PolishSpace α] : PolishSpace (ℕ → α) := inferInstance
#align polish_space.nat_fun PolishSpace.nat_fun

/-- A countable disjoint union of Polish spaces is Polish. -/
instance sigma {ι : Type*} [Countable ι] {E : ι → Type*} [∀ n, TopologicalSpace (E n)]
[∀ n, PolishSpace (E n)] : PolishSpace (Σn, E n) :=
Expand Down Expand Up @@ -159,6 +153,16 @@ theorem _root_.ClosedEmbedding.polishSpace [TopologicalSpace α] [TopologicalSpa
infer_instance
#align closed_embedding.polish_space ClosedEmbedding.polishSpace

/-- Any countable discrete space is Polish. -/
instance (priority := 50) polish_of_countable [TopologicalSpace α]
[h : Countable α] [DiscreteTopology α] : PolishSpace α := by
obtain ⟨f, hf⟩ := h.exists_injective_nat
have : ClosedEmbedding f := by
apply closedEmbedding_of_continuous_injective_closed continuous_of_discreteTopology hf
exact fun t _ => isClosed_discrete _
exact this.polishSpace
#align polish_of_countable PolishSpace.polish_of_countable

/-- Pulling back a Polish topology under an equiv gives again a Polish topology. -/
theorem _root_.Equiv.polishSpace_induced [t : TopologicalSpace β] [PolishSpace β] (f : α ≃ β) :
@PolishSpace α (t.induced f) :=
Expand All @@ -167,11 +171,16 @@ theorem _root_.Equiv.polishSpace_induced [t : TopologicalSpace β] [PolishSpace
#align equiv.polish_space_induced Equiv.polishSpace_induced

/-- A closed subset of a Polish space is also Polish. -/
theorem _root_.IsClosed.polishSpace {α : Type*} [TopologicalSpace α] [PolishSpace α] {s : Set α}
theorem _root_.IsClosed.polishSpace [TopologicalSpace α] [PolishSpace α] {s : Set α}
(hs : IsClosed s) : PolishSpace s :=
(IsClosed.closedEmbedding_subtype_val hs).polishSpace
#align is_closed.polish_space IsClosed.polishSpace

instance instPolishSpaceUniv [TopologicalSpace α] [PolishSpace α] :
PolishSpace (univ : Set α) :=
isClosed_univ.polishSpace
#align measure_theory.set.univ.polish_space PolishSpace.instPolishSpaceUniv

/-- A sequence of type synonyms of a given type `α`, useful in the proof of
`exists_polishSpace_forall_le` to endow each copy with a different topology. -/
@[nolint unusedArguments]
Expand Down