We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 603325b commit 854dbcdCopy full SHA for 854dbcd
1 file changed
Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
@@ -73,7 +73,7 @@ theorem ae_const_le_iff_forall_lt_measure_zero {β} [LinearOrder β] [Topologica
73
exact hc _ (u_lt n)
74
75
lemma ae_le_const_iff_forall_gt_measure_zero {β} [LinearOrder β] [TopologicalSpace β]
76
- [OrderTopology β] [FirstCountableTopology β] {μ : Measure α} {f : α → β} (c : β) :
+ [OrderTopology β] [FirstCountableTopology β] {μ : Measure α} (f : α → β) (c : β) :
77
(∀ᵐ x ∂μ, f x ≤ c) ↔ ∀ b, c < b → μ {x | b ≤ f x} = 0 :=
78
ae_const_le_iff_forall_lt_measure_zero (β := βᵒᵈ) _ _
79
0 commit comments