α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.827761
inst✝⁸ : MeasurableSpace α
K : Type ?u.827767
inst✝⁷ : SemilatticeSup β
inst✝⁶ : OrderBot β
inst✝⁵ : Zero β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderClosedTopology β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
inst✝ : MeasurableSpace γ
i : ℕ → β
f : γ → β
g : α → γ
n : ℕ
a : α
hf : Measurable f
hg : Measurable g
⊢ (Finset.sup (Finset.range n) fun k => if i k ≤ (f ∘ g) a then i k else 0) =
    Finset.sup (Finset.range n) fun k => if i k ≤ f (g a) then i k else 0
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.827761
inst✝⁸ : MeasurableSpace α
K : Type ?u.827767
inst✝⁷ : SemilatticeSup β
inst✝⁶ : OrderBot β
inst✝⁵ : Zero β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderClosedTopology β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
inst✝ : MeasurableSpace γ
i : ℕ → β
f : γ → β
g : α → γ
n : ℕ
a : α
hf : Measurable f
hg : Measurable g
⊢ ↑(approx i (f ∘ g) n) a = ↑(approx i f n) (g a)
rw [approx_apply _ hf, approx_apply _ (hf.comp hg)]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.827761
inst✝⁸ : MeasurableSpace α
K : Type ?u.827767
inst✝⁷ : SemilatticeSup β
inst✝⁶ : OrderBot β
inst✝⁵ : Zero β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderClosedTopology β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
inst✝ : MeasurableSpace γ
i : ℕ → β
f : γ → β
g : α → γ
n : ℕ
a : α
hf : Measurable f
hg : Measurable g
⊢ (Finset.sup (Finset.range n) fun k => if i k ≤ (f ∘ g) a then i k else 0) =
    Finset.sup (Finset.range n) fun k => if i k ≤ f (g a) then i k else 0
rfl