case h.e'_1
α : Type u_1
inst✝ : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ f = fun x => ⨆ (n : ℕ), ↑(eapprox f n) x

α : Type u_1
inst✝ : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), P ↑(eapprox f n)
α : Type u_1
inst✝ : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ P f
convert h_iSup (fun n => (eapprox f n).measurable) (monotone_eapprox f) _ using 1
case h.e'_1.h
α : Type u_1
inst✝ : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
x : α
⊢ f x = ⨆ (n : ℕ), ↑(eapprox f n) x
case h.e'_1
α : Type u_1
inst✝ : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ f = fun x => ⨆ (n : ℕ), ↑(eapprox f n) x
ext1 x
no goals
case h.e'_1.h
α : Type u_1
inst✝ : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
x : α
⊢ f x = ⨆ (n : ℕ), ↑(eapprox f n) x
rw [iSup_eapprox_apply f hf]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), P ↑(eapprox f n)
exact fun n =>
  SimpleFunc.induction (fun c s hs => h_ind c hs)
    (fun f g hfg hf hg => h_add hfg f.measurable g.measurable hf hg) (eapprox f n)