α : Type u_1
β : Type ?u.42415
γ : Type ?u.42418
δ : Type ?u.42421
ι : Type u_2
R : Type ?u.42427
R' : Type ?u.42430
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ¬Set.Nonempty (t i ∩ t j)
⊢ ∑ i in s, ↑↑μ (t i) ≤ ↑↑μ univ
α : Type u_1
β : Type ?u.42415
γ : Type ?u.42418
δ : Type ?u.42421
ι : Type u_2
R : Type ?u.42427
R' : Type ?u.42430
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : ↑↑μ univ < ∑ i in s, ↑↑μ (t i)
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ ∃ _h, Set.Nonempty (t i ∩ t j)
contrapose! H
α : Type u_1
β : Type ?u.42415
γ : Type ?u.42418
δ : Type ?u.42421
ι : Type u_2
R : Type ?u.42427
R' : Type ?u.42430
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ¬Set.Nonempty (t i ∩ t j)
⊢ PairwiseDisjoint ↑s fun i => t i
α : Type u_1
β : Type ?u.42415
γ : Type ?u.42418
δ : Type ?u.42421
ι : Type u_2
R : Type ?u.42427
R' : Type ?u.42430
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ¬Set.Nonempty (t i ∩ t j)
⊢ ∑ i in s, ↑↑μ (t i) ≤ ↑↑μ univ
apply sum_measure_le_measure_univ h
α : Type u_1
β : Type ?u.42415
γ : Type ?u.42418
δ : Type ?u.42421
ι : Type u_2
R : Type ?u.42427
R' : Type ?u.42430
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ¬Set.Nonempty (t i ∩ t j)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ (Disjoint on fun i => t i) i j
α : Type u_1
β : Type ?u.42415
γ : Type ?u.42418
δ : Type ?u.42421
ι : Type u_2
R : Type ?u.42427
R' : Type ?u.42430
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ¬Set.Nonempty (t i ∩ t j)
⊢ PairwiseDisjoint ↑s fun i => t i
intro i hi j hj hij
α : Type u_1
β : Type ?u.42415
γ : Type ?u.42418
δ : Type ?u.42421
ι : Type u_2
R : Type ?u.42427
R' : Type ?u.42430
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ¬Set.Nonempty (t i ∩ t j)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ t i ⊓ t j ≤ ⊥
α : Type u_1
β : Type ?u.42415
γ : Type ?u.42418
δ : Type ?u.42421
ι : Type u_2
R : Type ?u.42427
R' : Type ?u.42430
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ¬Set.Nonempty (t i ∩ t j)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ (Disjoint on fun i => t i) i j
rw [Function.onFun, disjoint_iff_inf_le]
no goals
α : Type u_1
β : Type ?u.42415
γ : Type ?u.42418
δ : Type ?u.42421
ι : Type u_2
R : Type ?u.42427
R' : Type ?u.42430
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ¬Set.Nonempty (t i ∩ t j)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ t i ⊓ t j ≤ ⊥
exact fun x hx => H i hi j hj hij ⟨x, hx⟩