α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ ↑(Finset.sup (Finset.range n) fun k => restrict (const α (i k)) {a | i k ≤ f a}) a =
    Finset.sup (Finset.range n) fun k => if i k ≤ f a then i k else 0
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ ↑(approx i f n) a = Finset.sup (Finset.range n) fun k => if i k ≤ f a then i k else 0
dsimp only [approx]
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ (Finset.sup (Finset.range n) fun c => ↑(restrict (const α (i c)) {a | i c ≤ f a}) a) =
    Finset.sup (Finset.range n) fun k => if i k ≤ f a then i k else 0
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ ↑(Finset.sup (Finset.range n) fun k => restrict (const α (i k)) {a | i k ≤ f a}) a =
    Finset.sup (Finset.range n) fun k => if i k ≤ f a then i k else 0
rw [finset_sup_apply]
case e_f
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ (fun c => ↑(restrict (const α (i c)) {a | i c ≤ f a}) a) = fun k => if i k ≤ f a then i k else 0
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ (Finset.sup (Finset.range n) fun c => ↑(restrict (const α (i c)) {a | i c ≤ f a}) a) =
    Finset.sup (Finset.range n) fun k => if i k ≤ f a then i k else 0
congr
case e_f.h
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ ↑(restrict (const α (i k)) {a | i k ≤ f a}) a = if i k ≤ f a then i k else 0
case e_f
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ (fun c => ↑(restrict (const α (i c)) {a | i c ≤ f a}) a) = fun k => if i k ≤ f a then i k else 0
funext k
case e_f.h
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ indicator {a | i k ≤ f a} (↑(const α (i k))) a = if i k ≤ f a then i k else 0

case e_f.h.hs
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ MeasurableSet {a | i k ≤ f a}
case e_f.h
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ ↑(restrict (const α (i k)) {a | i k ≤ f a}) a = if i k ≤ f a then i k else 0
rw [restrict_apply]
case e_f.h.hs
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ MeasurableSet {a | i k ≤ f a}
case e_f.h
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ indicator {a | i k ≤ f a} (↑(const α (i k))) a = if i k ≤ f a then i k else 0

case e_f.h.hs
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ MeasurableSet {a | i k ≤ f a}
rfl
no goals
case e_f.h.hs
α : Type u_2
β : Type u_1
γ : Type ?u.821186
δ : Type ?u.821189
inst✝⁷ : MeasurableSpace α
K : Type ?u.821195
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ MeasurableSet {a | i k ≤ f a}
exact hf measurableSet_Ici