case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
⊢ Measurable (uncurry u)
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
⊢ Measurable (uncurry u)
obtain ⟨t_sf, ht_sf⟩ :
  ∃ t : ℕ → SimpleFunc ι ι, ∀ j x, Tendsto (fun n => u (t n j) x) atTop (𝓝 <| u j x) := by
  have h_str_meas : StronglyMeasurable (id : ι → ι) := stronglyMeasurable_id
  refine' ⟨h_str_meas.approx, fun j x => _⟩
  exact ((hu_cont x).tendsto j).comp (h_str_meas.tendsto_approx j)
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
⊢ Measurable (uncurry u)
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
⊢ Measurable (uncurry u)
let U (n : ℕ) (p : ι × α) := u (t_sf n p.fst) p.snd
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
⊢ Measurable (uncurry u)
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
⊢ Measurable (uncurry u)
have h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd) := by
  rw [tendsto_pi_nhds]
  exact fun p => ht_sf p.fst p.snd
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
⊢ Measurable (U n)
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
⊢ Measurable (uncurry u)
refine' measurable_of_tendsto_metrizable (fun n => _) h_tendsto
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
h_meas : Measurable fun p => u (↑p.fst) p.snd
⊢ Measurable (U n)
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
⊢ Measurable (U n)
have h_meas : Measurable fun p : (t_sf n).range × α => u (↑p.fst) p.snd := by
  have :
    (fun p : ↥(t_sf n).range × α => u (↑p.fst) p.snd) =
      (fun p : α × (t_sf n).range => u (↑p.snd) p.fst) ∘ Prod.swap :=
    rfl
  rw [this, @measurable_swap_iff α (↥(t_sf n).range) β m]
  exact measurable_from_prod_countable fun j => h j
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
h_meas : Measurable fun p => u (↑p.fst) p.snd
this :
  (fun p => u (↑(t_sf n) p.fst) p.snd) =
    (fun p => u (↑p.fst) p.snd) ∘ fun p =>
      ({ val := ↑(t_sf n) p.fst, property := (_ : ↑(t_sf n) p.fst ∈ SimpleFunc.range (t_sf n)) }, p.snd)
⊢ Measurable (U n)
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
h_meas : Measurable fun p => u (↑p.fst) p.snd
⊢ Measurable (U n)
have :
  (fun p : ι × α => u (t_sf n p.fst) p.snd) =
    (fun p : ↥(t_sf n).range × α => u p.fst p.snd) ∘ fun p : ι × α =>
      (⟨t_sf n p.fst, SimpleFunc.mem_range_self _ _⟩, p.snd) :=
  rfl
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
h_meas : Measurable fun p => u (↑p.fst) p.snd
this :
  (fun p => u (↑(t_sf n) p.fst) p.snd) =
    (fun p => u (↑p.fst) p.snd) ∘ fun p =>
      ({ val := ↑(t_sf n) p.fst, property := (_ : ↑(t_sf n) p.fst ∈ SimpleFunc.range (t_sf n)) }, p.snd)
⊢ Measurable
    ((fun p => u (↑p.fst) p.snd) ∘ fun p =>
      ({ val := ↑(t_sf n) p.fst, property := (_ : ↑(t_sf n) p.fst ∈ SimpleFunc.range (t_sf n)) }, p.snd))
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
h_meas : Measurable fun p => u (↑p.fst) p.snd
this :
  (fun p => u (↑(t_sf n) p.fst) p.snd) =
    (fun p => u (↑p.fst) p.snd) ∘ fun p =>
      ({ val := ↑(t_sf n) p.fst, property := (_ : ↑(t_sf n) p.fst ∈ SimpleFunc.range (t_sf n)) }, p.snd)
⊢ Measurable (U n)
simp_rw [this]
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
h_meas : Measurable fun p => u (↑p.fst) p.snd
this :
  (fun p => u (↑(t_sf n) p.fst) p.snd) =
    (fun p => u (↑p.fst) p.snd) ∘ fun p =>
      ({ val := ↑(t_sf n) p.fst, property := (_ : ↑(t_sf n) p.fst ∈ SimpleFunc.range (t_sf n)) }, p.snd)
⊢ Measurable fun p => { val := ↑(t_sf n) p.fst, property := (_ : ↑(t_sf n) p.fst ∈ SimpleFunc.range (t_sf n)) }
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
h_meas : Measurable fun p => u (↑p.fst) p.snd
this :
  (fun p => u (↑(t_sf n) p.fst) p.snd) =
    (fun p => u (↑p.fst) p.snd) ∘ fun p =>
      ({ val := ↑(t_sf n) p.fst, property := (_ : ↑(t_sf n) p.fst ∈ SimpleFunc.range (t_sf n)) }, p.snd)
⊢ Measurable
    ((fun p => u (↑p.fst) p.snd) ∘ fun p =>
      ({ val := ↑(t_sf n) p.fst, property := (_ : ↑(t_sf n) p.fst ∈ SimpleFunc.range (t_sf n)) }, p.snd))
refine' h_meas.comp (Measurable.prod_mk _ measurable_snd)
no goals
case intro
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
h_meas : Measurable fun p => u (↑p.fst) p.snd
this :
  (fun p => u (↑(t_sf n) p.fst) p.snd) =
    (fun p => u (↑p.fst) p.snd) ∘ fun p =>
      ({ val := ↑(t_sf n) p.fst, property := (_ : ↑(t_sf n) p.fst ∈ SimpleFunc.range (t_sf n)) }, p.snd)
⊢ Measurable fun p => { val := ↑(t_sf n) p.fst, property := (_ : ↑(t_sf n) p.fst ∈ SimpleFunc.range (t_sf n)) }
exact ((t_sf n).measurable.comp measurable_fst).subtype_mk
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
h_str_meas : StronglyMeasurable id
⊢ ∃ t, ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t n) j) x) atTop (𝓝 (u j x))
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
⊢ ∃ t, ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t n) j) x) atTop (𝓝 (u j x))
have h_str_meas : StronglyMeasurable (id : ι → ι) := stronglyMeasurable_id
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
h_str_meas : StronglyMeasurable id
j : ι
x : α
⊢ Tendsto (fun n => u (↑(StronglyMeasurable.approx h_str_meas n) j) x) atTop (𝓝 (u j x))
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
h_str_meas : StronglyMeasurable id
⊢ ∃ t, ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t n) j) x) atTop (𝓝 (u j x))
refine' ⟨h_str_meas.approx, fun j x => _⟩
no goals
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
h_str_meas : StronglyMeasurable id
j : ι
x : α
⊢ Tendsto (fun n => u (↑(StronglyMeasurable.approx h_str_meas n) j) x) atTop (𝓝 (u j x))
exact ((hu_cont x).tendsto j).comp (h_str_meas.tendsto_approx j)
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
⊢ ∀ (x : ι × α), Tendsto (fun i => U i x) atTop (𝓝 (u x.fst x.snd))
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
⊢ Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
rw [tendsto_pi_nhds]
no goals
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
⊢ ∀ (x : ι × α), Tendsto (fun i => U i x) atTop (𝓝 (u x.fst x.snd))
exact fun p => ht_sf p.fst p.snd
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
this : (fun p => u (↑p.fst) p.snd) = (fun p => u (↑p.snd) p.fst) ∘ Prod.swap
⊢ Measurable fun p => u (↑p.fst) p.snd
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
⊢ Measurable fun p => u (↑p.fst) p.snd
have :
  (fun p : ↥(t_sf n).range × α => u (↑p.fst) p.snd) =
    (fun p : α × (t_sf n).range => u (↑p.snd) p.fst) ∘ Prod.swap :=
  rfl
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
this : (fun p => u (↑p.fst) p.snd) = (fun p => u (↑p.snd) p.fst) ∘ Prod.swap
⊢ Measurable fun p => u (↑p.snd) p.fst
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
this : (fun p => u (↑p.fst) p.snd) = (fun p => u (↑p.snd) p.fst) ∘ Prod.swap
⊢ Measurable fun p => u (↑p.fst) p.snd
rw [this, @measurable_swap_iff α (↥(t_sf n).range) β m]
no goals
α✝ : Type ?u.556281
β✝ : Type ?u.556284
γ : Type ?u.556287
ι✝ : Type ?u.556290
inst✝⁸ : Countable ι✝
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.fst) p.snd
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd)
n : ℕ
this : (fun p => u (↑p.fst) p.snd) = (fun p => u (↑p.snd) p.fst) ∘ Prod.swap
⊢ Measurable fun p => u (↑p.snd) p.fst
exact measurable_from_prod_countable fun j => h j