α : Type u_1
β : Type ?u.30507
γ : Type ?u.30510
δ : Type ?u.30513
ι : Type ?u.30516
R : Type ?u.30519
R' : Type ?u.30522
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ s ∪ t =ᵐ[μ] s ↔ ↑↑μ (t \ s) = 0
α : Type u_1
β : Type ?u.30507
γ : Type ?u.30510
δ : Type ?u.30513
ι : Type ?u.30516
R : Type ?u.30519
R' : Type ?u.30522
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ s ∪ t =ᵐ[μ] s ↔ t ≤ᵐ[μ] s
rw [ae_le_set]
no goals
α : Type u_1
β : Type ?u.30507
γ : Type ?u.30510
δ : Type ?u.30513
ι : Type ?u.30516
R : Type ?u.30519
R' : Type ?u.30522
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ s ∪ t =ᵐ[μ] s ↔ ↑↑μ (t \ s) = 0
refine'
  ⟨fun h => by simpa only [union_diff_left] using (ae_eq_set.mp h).1, fun h =>
    eventuallyLE_antisymm_iff.mpr
      ⟨by rwa [ae_le_set, union_diff_left],
        HasSubset.Subset.eventuallyLE <| subset_union_left s t⟩⟩
no goals
α : Type u_1
β : Type ?u.30507
γ : Type ?u.30510
δ : Type ?u.30513
ι : Type ?u.30516
R : Type ?u.30519
R' : Type ?u.30522
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : s ∪ t =ᵐ[μ] s
⊢ ↑↑μ (t \ s) = 0
simpa only [union_diff_left] using (ae_eq_set.mp h).1
no goals
α : Type u_1
β : Type ?u.30507
γ : Type ?u.30510
δ : Type ?u.30513
ι : Type ?u.30516
R : Type ?u.30519
R' : Type ?u.30522
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : ↑↑μ (t \ s) = 0
⊢ s ∪ t ≤ᵐ[μ] s
rwa [ae_le_set, union_diff_left]