α : Type u_1
β : Type ?u.38719
inst✝³ : MeasurableSpace α
M : Type ?u.38725
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h : n ≠ m
⊢ (Disjoint on MeasureTheory.SignedMeasure.restrictNonposSeq s i) n m
α : Type u_1
β : Type ?u.38719
inst✝³ : MeasurableSpace α
M : Type ?u.38725
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
⊢ Pairwise (Disjoint on MeasureTheory.SignedMeasure.restrictNonposSeq s i)
intro n m h
α : Type u_1
β : Type ?u.38719
inst✝³ : MeasurableSpace α
M : Type ?u.38725
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h : n ≠ m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅
α : Type u_1
β : Type ?u.38719
inst✝³ : MeasurableSpace α
M : Type ?u.38725
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h : n ≠ m
⊢ (Disjoint on MeasureTheory.SignedMeasure.restrictNonposSeq s i) n m
rw [Function.onFun, Set.disjoint_iff_inter_eq_empty]
case inl
α : Type u_1
β : Type ?u.38719
inst✝³ : MeasurableSpace α
M : Type ?u.38725
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h✝ : n ≠ m
h : n < m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅

case inr
α : Type u_1
β : Type ?u.38719
inst✝³ : MeasurableSpace α
M : Type ?u.38725
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h✝ : n ≠ m
h : n > m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅
α : Type u_1
β : Type ?u.38719
inst✝³ : MeasurableSpace α
M : Type ?u.38725
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h : n ≠ m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅
rcases lt_or_gt_of_ne h with (h | h)
no goals
case inl
α : Type u_1
β : Type ?u.38719
inst✝³ : MeasurableSpace α
M : Type ?u.38725
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h✝ : n ≠ m
h : n < m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅
rw [restrictNonposSeq_disjoint' h]
no goals
case inr
α : Type u_1
β : Type ?u.38719
inst✝³ : MeasurableSpace α
M : Type ?u.38725
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h✝ : n ≠ m
h : n > m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅
rw [Set.inter_comm, restrictNonposSeq_disjoint' h]