α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬Set.Countable C
this : UpgradedPolishSpace α := upgradePolishSpace α
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬Set.Countable C
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f
letI := upgradePolishSpace α
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬Set.Countable C
this : UpgradedPolishSpace α := upgradePolishSpace α
D : Set α
hD : Perfect D
Dnonempty : Set.Nonempty D
hDC : D ⊆ C
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬Set.Countable C
this : UpgradedPolishSpace α := upgradePolishSpace α
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f
obtain ⟨D, hD, Dnonempty, hDC⟩ := exists_perfect_nonempty_of_isClosed_of_not_countable hC hunc
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬Set.Countable C
this : UpgradedPolishSpace α := upgradePolishSpace α
D : Set α
hD : Perfect D
Dnonempty : Set.Nonempty D
hDC : D ⊆ C
f : (ℕ → Bool) → α
hfD : range f ⊆ D
hf : Continuous f ∧ Function.Injective f
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬Set.Countable C
this : UpgradedPolishSpace α := upgradePolishSpace α
D : Set α
hD : Perfect D
Dnonempty : Set.Nonempty D
hDC : D ⊆ C
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f
obtain ⟨f, hfD, hf⟩ := hD.exists_nat_bool_injection Dnonempty
no goals
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬Set.Countable C
this : UpgradedPolishSpace α := upgradePolishSpace α
D : Set α
hD : Perfect D
Dnonempty : Set.Nonempty D
hDC : D ⊆ C
f : (ℕ → Bool) → α
hfD : range f ⊆ D
hf : Continuous f ∧ Function.Injective f
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f
exact ⟨f, hfD.trans hDC, hf⟩