case intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
⊢ ↑↑μ (⋂ (i : ι), s i) = ⨅ (i : ι), ↑↑μ (s i)
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
hfin : ∃ i, ↑↑μ (s i) ≠ ⊤
⊢ ↑↑μ (⋂ (i : ι), s i) = ⨅ (i : ι), ↑↑μ (s i)
rcases hfin with ⟨k, hk⟩
case intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
⊢ ↑↑μ (⋂ (i : ι), s i) = ⨅ (i : ι), ↑↑μ (s i)
case intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
⊢ ↑↑μ (⋂ (i : ι), s i) = ⨅ (i : ι), ↑↑μ (s i)
have : ∀ (t) (_ : t ⊆ s k), μ t ≠ ∞ := fun t ht => ne_top_of_le_ne_top hk (measure_mono ht)
case intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
⊢ (↑↑μ (s k) - ⨆ (i : ι), ↑↑μ (s k \ s i)) = ↑↑μ (s k) - ⨆ (i : ι), ↑↑μ (s k) - ↑↑μ (s i)

case intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i => s k \ s i
case intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
⊢ ↑↑μ (⋂ (i : ι), s i) = ⨅ (i : ι), ↑↑μ (s i)
rw [← ENNReal.sub_sub_cancel hk (iInf_le _ k), ENNReal.sub_iInf, ←
  ENNReal.sub_sub_cancel hk (measure_mono (iInter_subset _ k)), ←
  measure_diff (iInter_subset _ k) (MeasurableSet.iInter h) (this _ (iInter_subset _ k)),
  diff_iInter, measure_iUnion_eq_iSup]
case intro.e_a
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
⊢ (⨆ (i : ι), ↑↑μ (s k \ s i)) = ⨆ (i : ι), ↑↑μ (s k) - ↑↑μ (s i)
case intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
⊢ (↑↑μ (s k) - ⨆ (i : ι), ↑↑μ (s k \ s i)) = ↑↑μ (s k) - ⨆ (i : ι), ↑↑μ (s k) - ↑↑μ (s i)
congr 1
case intro.e_a.refine'_1
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ ∃ i', ↑↑μ (s k \ s i) ≤ ↑↑μ (s k) - ↑↑μ (s i')

case intro.e_a.refine'_2
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ ↑↑μ (s k) - ↑↑μ (s i) ≤ ↑↑μ (s k \ s i)
case intro.e_a
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
⊢ (⨆ (i : ι), ↑↑μ (s k \ s i)) = ⨆ (i : ι), ↑↑μ (s k) - ↑↑μ (s i)
refine' le_antisymm (iSup_mono' fun i => _) (iSup_mono fun i => _)
case intro.e_a.refine'_1.intro.intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ ∃ i', ↑↑μ (s k \ s i) ≤ ↑↑μ (s k) - ↑↑μ (s i')
case intro.e_a.refine'_1
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ ∃ i', ↑↑μ (s k \ s i) ≤ ↑↑μ (s k) - ↑↑μ (s i')
rcases hd i k with ⟨j, hji, hjk⟩
case intro.e_a.refine'_1.intro.intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ ↑↑μ (s k \ s i) ≤ ↑↑μ (s k) - ↑↑μ (s j)
case intro.e_a.refine'_1.intro.intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ ∃ i', ↑↑μ (s k \ s i) ≤ ↑↑μ (s k) - ↑↑μ (s i')
use j
case intro.e_a.refine'_1.intro.intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ ↑↑μ (s k \ s i) ≤ ↑↑μ (s k \ s j)
case intro.e_a.refine'_1.intro.intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ ↑↑μ (s k \ s i) ≤ ↑↑μ (s k) - ↑↑μ (s j)
rw [← measure_diff hjk (h _) (this _ hjk)]
no goals
case intro.e_a.refine'_1.intro.intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ ↑↑μ (s k \ s i) ≤ ↑↑μ (s k \ s j)
exact measure_mono (diff_subset_diff_right hji)
case intro.e_a.refine'_2
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ ↑↑μ (s k) ≤ ↑↑μ (s i ∪ s k \ s i)

case intro.e_a.refine'_2.hd
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ Disjoint (s k \ s i) (s i)

case intro.e_a.refine'_2.h
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ MeasurableSet (s i)
case intro.e_a.refine'_2
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ ↑↑μ (s k) - ↑↑μ (s i) ≤ ↑↑μ (s k \ s i)
rw [tsub_le_iff_right, ← measure_union, Set.union_comm]
case intro.e_a.refine'_2.hd
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ Disjoint (s k \ s i) (s i)

case intro.e_a.refine'_2.h
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ MeasurableSet (s i)
case intro.e_a.refine'_2
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ ↑↑μ (s k) ≤ ↑↑μ (s i ∪ s k \ s i)

case intro.e_a.refine'_2.hd
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ Disjoint (s k \ s i) (s i)

case intro.e_a.refine'_2.h
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ MeasurableSet (s i)
exact measure_mono (diff_subset_iff.1 <| Subset.refl _)
case intro.e_a.refine'_2.h
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ MeasurableSet (s i)
case intro.e_a.refine'_2.hd
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ Disjoint (s k \ s i) (s i)

case intro.e_a.refine'_2.h
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ MeasurableSet (s i)
apply disjoint_sdiff_left
no goals
case intro.e_a.refine'_2.h
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
i : ι
⊢ MeasurableSet (s i)
apply h i
no goals
case intro
α : Type u_2
β : Type ?u.53347
γ : Type ?u.53350
δ : Type ?u.53353
ι : Type u_1
R : Type ?u.53359
R' : Type ?u.53362
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), MeasurableSet (s i)
hd : Directed (fun x x_1 => x ⊇ x_1) s
k : ι
hk : ↑↑μ (s k) ≠ ⊤
this : ∀ (t : Set α), t ⊆ s k → ↑↑μ t ≠ ⊤
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i => s k \ s i
exact hd.mono_comp _ fun _ _ => diff_subset_diff_right