case h.e'_5.h
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
x✝ : δ
⊢ (⨅ (_ : p), f x✝) = f x✝
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
⊢ Measurable fun b => ⨅ (_ : p), f b
convert hf
case h.e'_5.h
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
x✝ : δ
⊢ (⨅ (_ : p), f x✝) = f x✝
case h.e'_5.h
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
x✝ : δ
⊢ (⨅ (_ : p), f x✝) = f x✝
funext
no goals
case h.e'_5.h
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
x✝ : δ
⊢ (⨅ (_ : p), f x✝) = f x✝
exact iInf_pos h
case h.e'_5
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ (fun b => ⨅ (_ : p), f b) = fun x => ?convert_5

case convert_5
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ α
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ Measurable fun b => ⨅ (_ : p), f b
convert measurable_const using 1
case h.e'_5.h
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
x✝ : δ
⊢ (⨅ (_ : p), f x✝) = ?convert_5

case convert_5
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ α
case h.e'_5
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ (fun b => ⨅ (_ : p), f b) = fun x => ?convert_5

case convert_5
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ α
funext
no goals
case h.e'_5.h
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
x✝ : δ
⊢ (⨅ (_ : p), f x✝) = ?convert_5

case convert_5
α✝ : Type ?u.1409247
β : Type ?u.1409250
γ : Type ?u.1409253
γ₂ : Type ?u.1409256
δ : Type u_2
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
inst✝¹⁰ : MeasurableSpace α✝
inst✝⁹ : BorelSpace α✝
inst✝⁸ : TopologicalSpace β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : BorelSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : MeasurableSpace γ
inst✝³ : BorelSpace γ
inst✝² : MeasurableSpace δ
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ α
exact iInf_neg h