α : Type u_1
β : Type ?u.56687
γ : Type ?u.56690
δ : Type ?u.56693
δ' : Type ?u.56696
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet ((fun x => Nat.find (_ : ∃ N, p x N)) ⁻¹' {Nat.find (_ : ∃ N, p x N)})
α : Type u_1
β : Type ?u.56687
γ : Type ?u.56690
δ : Type ?u.56693
δ' : Type ?u.56696
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
⊢ Measurable fun x => Nat.find (_ : ∃ N, p x N)
refine' measurable_to_nat fun x => _
α : Type u_1
β : Type ?u.56687
γ : Type ?u.56690
δ : Type ?u.56693
δ' : Type ?u.56696
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet (disjointed (fun k => {x | p x k}) (Nat.find (_ : ∃ N, p x N)))
α : Type u_1
β : Type ?u.56687
γ : Type ?u.56690
δ : Type ?u.56693
δ' : Type ?u.56696
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet ((fun x => Nat.find (_ : ∃ N, p x N)) ⁻¹' {Nat.find (_ : ∃ N, p x N)})
rw [preimage_find_eq_disjointed (fun k => {x | p x k})]
no goals
α : Type u_1
β : Type ?u.56687
γ : Type ?u.56690
δ : Type ?u.56693
δ' : Type ?u.56696
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet (disjointed (fun k => {x | p x k}) (Nat.find (_ : ∃ N, p x N)))
exact MeasurableSet.disjointed hm _