α : Type u_1
β : Type ?u.41179
γ : Type ?u.41182
δ : Type ?u.41185
ι : Type u_2
R : Type ?u.41191
R' : Type ?u.41194
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : ∀ (i j : ι), i ≠ j → ¬Set.Nonempty (s i ∩ s j)
⊢ (∑' (i : ι), ↑↑μ (s i)) ≤ ↑↑μ univ
α : Type u_1
β : Type ?u.41179
γ : Type ?u.41182
δ : Type ?u.41185
ι : Type u_2
R : Type ?u.41191
R' : Type ?u.41194
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : ↑↑μ univ < ∑' (i : ι), ↑↑μ (s i)
⊢ ∃ i j _h, Set.Nonempty (s i ∩ s j)
contrapose! H
α : Type u_1
β : Type ?u.41179
γ : Type ?u.41182
δ : Type ?u.41185
ι : Type u_2
R : Type ?u.41191
R' : Type ?u.41194
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : ∀ (i j : ι), i ≠ j → ¬Set.Nonempty (s i ∩ s j)
⊢ Pairwise (Disjoint on fun i => s i)
α : Type u_1
β : Type ?u.41179
γ : Type ?u.41182
δ : Type ?u.41185
ι : Type u_2
R : Type ?u.41191
R' : Type ?u.41194
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : ∀ (i j : ι), i ≠ j → ¬Set.Nonempty (s i ∩ s j)
⊢ (∑' (i : ι), ↑↑μ (s i)) ≤ ↑↑μ univ
apply tsum_measure_le_measure_univ hs
α : Type u_1
β : Type ?u.41179
γ : Type ?u.41182
δ : Type ?u.41185
ι : Type u_2
R : Type ?u.41191
R' : Type ?u.41194
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : ∀ (i j : ι), i ≠ j → ¬Set.Nonempty (s i ∩ s j)
i j : ι
hij : i ≠ j
⊢ (Disjoint on fun i => s i) i j
α : Type u_1
β : Type ?u.41179
γ : Type ?u.41182
δ : Type ?u.41185
ι : Type u_2
R : Type ?u.41191
R' : Type ?u.41194
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : ∀ (i j : ι), i ≠ j → ¬Set.Nonempty (s i ∩ s j)
⊢ Pairwise (Disjoint on fun i => s i)
intro i j hij
α : Type u_1
β : Type ?u.41179
γ : Type ?u.41182
δ : Type ?u.41185
ι : Type u_2
R : Type ?u.41191
R' : Type ?u.41194
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : ∀ (i j : ι), i ≠ j → ¬Set.Nonempty (s i ∩ s j)
i j : ι
hij : i ≠ j
⊢ s i ⊓ s j ≤ ⊥
α : Type u_1
β : Type ?u.41179
γ : Type ?u.41182
δ : Type ?u.41185
ι : Type u_2
R : Type ?u.41191
R' : Type ?u.41194
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : ∀ (i j : ι), i ≠ j → ¬Set.Nonempty (s i ∩ s j)
i j : ι
hij : i ≠ j
⊢ (Disjoint on fun i => s i) i j
rw [Function.onFun, disjoint_iff_inf_le]
no goals
α : Type u_1
β : Type ?u.41179
γ : Type ?u.41182
δ : Type ?u.41185
ι : Type u_2
R : Type ?u.41191
R' : Type ?u.41194
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : ∀ (i j : ι), i ≠ j → ¬Set.Nonempty (s i ∩ s j)
i j : ι
hij : i ≠ j
⊢ s i ⊓ s j ≤ ⊥
exact fun x hx => H i j hij ⟨x, hx⟩