case inl
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : IsEmpty ι
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α

case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
rcases isEmpty_or_nonempty ι with (hι | hι)
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
inhabit ι
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
letI : ∀ n : ι, TopologicalSpace (AuxCopy α n) := fun n => m n
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
haveI : ∀ n : ι, PolishSpace (AuxCopy α n) := fun n => h'm n
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
letI T : TopologicalSpace (∀ n : ι, AuxCopy α n) := inferInstance
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
let f : α → ∀ n : ι, AuxCopy α n := fun x _ => x
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
have T_le_m : ∀ n, T.induced f ≤ m n := fun n ↦ by
  rw [induced_to_pi]
  exact iInf_le_of_le n (@induced_id _ (m n)).le
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
⊢ PolishSpace α
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
refine' ⟨T.induced f, fun n => T_le_m n, (T_le_m default).trans (hm default), _⟩
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
⊢ PolishSpace α
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
⊢ PolishSpace α
have f_closed : IsClosed (range f) := by
  rw [A]
  refine isClosed_iInter fun n => ?_
  have C : ∀ i : ι, Continuous fun x : ∀ n, AuxCopy α n => (id (x i) : α) := fun i ↦
    have : Continuous (show AuxCopy α i → α from id) := continuous_id_of_le (hm i)
    this.comp (continuous_apply i)
  apply isClosed_eq (C n) (C default)
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
K : _root_.Embedding f
⊢ PolishSpace α
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
⊢ PolishSpace α
have K : @_root_.Embedding _ _ (T.induced f) T f := by
  refine Function.Injective.embedding_induced fun x y hxy ↦ ?_
  have : f x default = f y default := by rw [hxy]
  exact this
no goals
case inr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
K : _root_.Embedding f
L : ClosedEmbedding f
⊢ PolishSpace α
exact @ClosedEmbedding.polishSpace _ _ (T.induced f) T (by infer_instance) _ L
no goals
case inl
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : IsEmpty ι
⊢ ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
exact ⟨t, fun i => (IsEmpty.elim hι i : _), le_rfl, p⟩
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
n : ι
⊢ (⨅ (i : ι), induced (fun x => f x i) inferInstance) ≤ m n
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
n : ι
⊢ induced f T ≤ m n
rw [induced_to_pi]
no goals
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
n : ι
⊢ (⨅ (i : ι), induced (fun x => f x i) inferInstance) ≤ m n
exact iInf_le_of_le n (@induced_id _ (m n)).le
case h
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
⊢ x ∈ range f ↔ x ∈ ⋂ (n : ι), {x | x n = x default}
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
⊢ range f = ⋂ (n : ι), {x | x n = x default}
ext x
case h.mp
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
⊢ x ∈ range f → x ∈ ⋂ (n : ι), {x | x n = x default}

case h.mpr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
⊢ (x ∈ ⋂ (n : ι), {x | x n = x default}) → x ∈ range f
case h
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
⊢ x ∈ range f ↔ x ∈ ⋂ (n : ι), {x | x n = x default}
constructor
case h.mp.intro
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
y : α
⊢ f y ∈ ⋂ (n : ι), {x | x n = x default}
case h.mp
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
⊢ x ∈ range f → x ∈ ⋂ (n : ι), {x | x n = x default}
rintro ⟨y, rfl⟩
no goals
case h.mp.intro
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
y : α
⊢ f y ∈ ⋂ (n : ι), {x | x n = x default}
exact mem_iInter.2 fun n => by simp only [mem_setOf_eq]
no goals
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
y : α
n : ι
⊢ f y ∈ {x | x n = x default}
simp only [mem_setOf_eq]
case h.mpr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
hx : x ∈ ⋂ (n : ι), {x | x n = x default}
⊢ f (x default) = x
case h.mpr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
⊢ (x ∈ ⋂ (n : ι), {x | x n = x default}) → x ∈ range f
refine fun hx ↦ ⟨x default, ?_⟩
case h.mpr.h
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
hx : x ∈ ⋂ (n : ι), {x | x n = x default}
n : ι
⊢ f (x default) n = x n
case h.mpr
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
hx : x ∈ ⋂ (n : ι), {x | x n = x default}
⊢ f (x default) = x
ext1 n
case h.mpr.h
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
hx : x ∈ ⋂ (n : ι), {x | x n = x default}
n : ι
⊢ x n = f (x default) n
case h.mpr.h
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
hx : x ∈ ⋂ (n : ι), {x | x n = x default}
n : ι
⊢ f (x default) n = x n
symm
no goals
case h.mpr.h
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
x : (n : ι) → AuxCopy α n
hx : x ∈ ⋂ (n : ι), {x | x n = x default}
n : ι
⊢ x n = f (x default) n
exact mem_iInter.1 hx n
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
⊢ IsClosed (⋂ (n : ι), {x | x n = x default})
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
⊢ IsClosed (range f)
rw [A]
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
n : ι
⊢ IsClosed {x | x n = x default}
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
⊢ IsClosed (⋂ (n : ι), {x | x n = x default})
refine isClosed_iInter fun n => ?_
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
n : ι
C : ∀ (i : ι), Continuous fun x => id (x i)
⊢ IsClosed {x | x n = x default}
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
n : ι
⊢ IsClosed {x | x n = x default}
have C : ∀ i : ι, Continuous fun x : ∀ n, AuxCopy α n => (id (x i) : α) := fun i ↦
  have : Continuous (show AuxCopy α i → α from id) := continuous_id_of_le (hm i)
  this.comp (continuous_apply i)
no goals
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
n : ι
C : ∀ (i : ι), Continuous fun x => id (x i)
⊢ IsClosed {x | x n = x default}
apply isClosed_eq (C n) (C default)
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
x y : α
hxy : f x = f y
⊢ x = y
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
⊢ _root_.Embedding f
refine Function.Injective.embedding_induced fun x y hxy ↦ ?_
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝¹ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this✝ : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
x y : α
hxy : f x = f y
this : f x default = f y default
⊢ x = y
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
x y : α
hxy : f x = f y
⊢ x = y
have : f x default = f y default := by rw [hxy]
no goals
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝¹ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this✝ : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
x y : α
hxy : f x = f y
this : f x default = f y default
⊢ x = y
exact this
no goals
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
x y : α
hxy : f x = f y
⊢ f x default = f y default
rw [hxy]
case refine_1
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
K : _root_.Embedding f
⊢ _root_.Embedding f

case refine_2
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
K : _root_.Embedding f
⊢ IsClosed (range f)
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
K : _root_.Embedding f
⊢ ClosedEmbedding f
refine @ClosedEmbedding.mk _ _ (T.induced f) T f ?_ ?_
no goals
case refine_1
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
K : _root_.Embedding f
⊢ _root_.Embedding f
exact K
no goals
case refine_2
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
K : _root_.Embedding f
⊢ IsClosed (range f)
exact f_closed
no goals
α : Type u_2
β : Type ?u.8502
ι : Type u_1
inst✝ : Countable ι
t : TopologicalSpace α
p : PolishSpace α
m : ι → TopologicalSpace α
hm : ∀ (n : ι), m n ≤ t
h'm : ∀ (n : ι), PolishSpace α
hι : Nonempty ι
inhabited_h : Inhabited ι
this✝ : (n : ι) → TopologicalSpace (AuxCopy α n) := fun n => m n
this : ∀ (n : ι), PolishSpace (AuxCopy α n)
T : TopologicalSpace ((n : ι) → AuxCopy α n) := inferInstance
f : α → (n : ι) → AuxCopy α n := fun x x_1 => x
T_le_m : ∀ (n : ι), induced f T ≤ m n
A : range f = ⋂ (n : ι), {x | x n = x default}
f_closed : IsClosed (range f)
K : _root_.Embedding f
L : ClosedEmbedding f
⊢ PolishSpace ((n : ι) → AuxCopy α n)
infer_instance