Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
⊢ Indep (limsup s atBot) (limsup s atBot)
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
⊢ Indep (limsup s atBot) (limsup s atBot)
let ns : ι → Set ι := Set.Ici
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Indep (limsup s atBot) (limsup s atBot)
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
⊢ Indep (limsup s atBot) (limsup s atBot)
have hnsp : ∀ i, BddBelow (ns i) := fun i => bddBelow_Ici
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (t : Set ι), BddBelow t → tᶜ ∈ atBot

case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Directed (fun x x_1 => x ≤ x_1) fun a => ns a

case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Indep (limsup s atBot) (limsup s atBot)
refine' indep_limsup_self h_le h_indep _ _ hnsp _
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (t : Set ι), (∃ x, x ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}) → ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (t : Set ι), BddBelow t → tᶜ ∈ atBot
simp only [mem_atBot_sets, ge_iff_le, Set.mem_compl_iff, BddBelow, lowerBounds, Set.Nonempty]
case refine'_1.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
⊢ ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (t : Set ι), (∃ x, x ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}) → ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
rintro t ⟨a, ha⟩
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
⊢ ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
case refine'_1.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
⊢ ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
obtain ⟨b, hb⟩ : ∃ b, b < a := exists_lt a
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ False
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
⊢ ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
refine' ⟨b, fun c hc hct => _⟩
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
this : ∀ (i : ι), i ∈ t → c < i
⊢ False

case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → c < i
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ False
suffices : ∀ i ∈ t, c < i
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → c < i
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
this : ∀ (i : ι), i ∈ t → c < i
⊢ False

case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → c < i
exact lt_irrefl c (this c hct)
no goals
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → c < i
exact fun i hi => hc.trans_lt (hb.trans_le (ha hi))
no goals
case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Directed (fun x x_1 => x ≤ x_1) fun a => ns a
exact directed_of_inf fun i j hij k hki => hij.trans hki
no goals
case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a
exact fun n => ⟨n, le_rfl⟩