α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
⊢ AnalyticSet (⋃ (n : ι), s n)
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
⊢ AnalyticSet (⋃ (n : ι), s n)
choose β hβ h'β f f_cont f_range using fun n =>
  analyticSet_iff_exists_polishSpace_range.1 (hs n)
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
⊢ AnalyticSet (⋃ (n : ι), s n)
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
⊢ AnalyticSet (⋃ (n : ι), s n)
skip
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
⊢ AnalyticSet (⋃ (n : ι), s n)
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
⊢ AnalyticSet (⋃ (n : ι), s n)
let γ := Σn, β n
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
⊢ AnalyticSet (⋃ (n : ι), s n)
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
⊢ AnalyticSet (⋃ (n : ι), s n)
let F : γ → α := by
  rintro ⟨n, x⟩
  exact f n x
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
⊢ AnalyticSet (⋃ (n : ι), s n)
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
⊢ AnalyticSet (⋃ (n : ι), s n)
have F_cont : Continuous F := continuous_sigma f_cont
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
F_range : range F = ⋃ (n : ι), s n
⊢ AnalyticSet (⋃ (n : ι), s n)
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
⊢ AnalyticSet (⋃ (n : ι), s n)
have F_range : range F = ⋃ n, s n := by
  rw [range_sigma_eq_iUnion_range]
  apply congr_arg
  ext1 n
  rw [← f_range n]
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
F_range : range F = ⋃ (n : ι), s n
⊢ AnalyticSet (range F)
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
F_range : range F = ⋃ (n : ι), s n
⊢ AnalyticSet (⋃ (n : ι), s n)
rw [← F_range]
no goals
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
F_range : range F = ⋃ (n : ι), s n
⊢ AnalyticSet (range F)
exact analyticSet_range_of_polishSpace F_cont
case mk
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
n : ι
x : β n
⊢ α
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
⊢ γ → α
rintro ⟨n, x⟩
no goals
case mk
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
n : ι
x : β n
⊢ α
exact f n x
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
⊢ (⋃ (a : ι), range fun b => F { fst := a, snd := b }) = ⋃ (n : ι), s n
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
⊢ range F = ⋃ (n : ι), s n
rw [range_sigma_eq_iUnion_range]
case h
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
⊢ (fun a => range fun b => F { fst := a, snd := b }) = fun n => s n
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
⊢ (⋃ (a : ι), range fun b => F { fst := a, snd := b }) = ⋃ (n : ι), s n
apply congr_arg
case h.h
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
n : ι
⊢ (range fun b => F { fst := n, snd := b }) = s n
case h
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
⊢ (fun a => range fun b => F { fst := a, snd := b }) = fun n => s n
ext1 n
no goals
case h.h
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_1 := (n : ι) × β n
F : γ → α := fun a => Sigma.casesOn a fun n x => f n x
F_cont : Continuous F
n : ι
⊢ (range fun b => F { fst := n, snd := b }) = s n
rw [← f_range n]