α : Type u_1
β : Type ?u.326296
γ : Type ?u.326299
δ : Type ?u.326302
ι : Type ?u.326305
R : Type ?u.326308
R' : Type ?u.326311
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s = 1
α : Type u_1
β : Type ?u.326296
γ : Type ?u.326299
δ : Type ?u.326302
ι : Type ?u.326305
R : Type ?u.326308
R' : Type ?u.326311
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
a : α
h : a ∈ s
⊢ ↑↑(dirac a) s = 1
have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1
α : Type u_1
β : Type ?u.326296
γ : Type ?u.326299
δ : Type ?u.326302
ι : Type ?u.326305
R : Type ?u.326308
R' : Type ?u.326311
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s ≤ indicator univ 1 a
α : Type u_1
β : Type ?u.326296
γ : Type ?u.326299
δ : Type ?u.326302
ι : Type ?u.326305
R : Type ?u.326308
R' : Type ?u.326311
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s = 1
refine' le_antisymm (this univ trivial ▸ _) (this s h ▸ le_dirac_apply)
α : Type u_1
β : Type ?u.326296
γ : Type ?u.326299
δ : Type ?u.326302
ι : Type ?u.326305
R : Type ?u.326308
R' : Type ?u.326311
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s ≤ ↑↑(dirac a) univ
α : Type u_1
β : Type ?u.326296
γ : Type ?u.326299
δ : Type ?u.326302
ι : Type ?u.326305
R : Type ?u.326308
R' : Type ?u.326311
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s ≤ indicator univ 1 a
rw [← dirac_apply' a MeasurableSet.univ]
no goals
α : Type u_1
β : Type ?u.326296
γ : Type ?u.326299
δ : Type ?u.326302
ι : Type ?u.326305
R : Type ?u.326308
R' : Type ?u.326311
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → indicator t 1 a = 1
⊢ ↑↑(dirac a) s ≤ ↑↑(dirac a) univ
exact measure_mono (subset_univ s)