Theorem: aEMeasurable_liminf' (Ray/Misc/Measure.lean)

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
⊢ AEMeasurable (fun x => liminf (fun n => f n x) u) μ
Tactic:
simp_rw [uc.toHasBasis.liminf_eq_iSup_iInf]
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
⊢ AEMeasurable (fun x => ⨆ i, ⨆ (_ : p i), ⨅ a ∈ s i, f a x) μ

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
⊢ AEMeasurable (fun x => ⨆ i, ⨆ (_ : p i), ⨅ a ∈ s i, f a x) μ
Tactic:
refine aemeasurable_biSup _ uc.countable ?_
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
⊢ ∀ i ∈ fun i => p i, AEMeasurable (fun x => ⨅ a ∈ s i, f a x) μ

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
⊢ ∀ i ∈ fun i => p i, AEMeasurable (fun x => ⨅ a ∈ s i, f a x) μ
Tactic:
intro i _
State after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
i : I'
a✝ : i ∈ fun i => p i
⊢ AEMeasurable (fun x => ⨅ a ∈ s i, f a x) μ

State before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
i : I'
a✝ : i ∈ fun i => p i
⊢ AEMeasurable (fun x => ⨅ a ∈ s i, f a x) μ
Tactic:
exact aemeasurable_biInf _ (sc i) (fun n _ ↦ fm n)
State after:
no goals