α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ ↑↑μ {a | ¬c ≤ f a} = 0 ↔ ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ (∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
rw [ae_iff]
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ ↑↑μ {a | f a < c} = 0 ↔ ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ ↑↑μ {a | ¬c ≤ f a} = 0 ↔ ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
push_neg
case mp
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ ↑↑μ {a | f a < c} = 0 → ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0

case mpr
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ (∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0) → ↑↑μ {a | f a < c} = 0
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ ↑↑μ {a | f a < c} = 0 ↔ ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
constructor
case mpr
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
⊢ ↑↑μ {a | f a < c} = 0
case mpr
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ (∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0) → ↑↑μ {a | f a < c} = 0
intro hc
case pos
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ∀ (b : β), c ≤ b
⊢ ↑↑μ {a | f a < c} = 0

case neg
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
⊢ ↑↑μ {a | f a < c} = 0
case mpr
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
⊢ ↑↑μ {a | f a < c} = 0
by_cases h : ∀ b, c ≤ b
case pos
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
H : ¬IsLUB (Set.Iio c) c
⊢ ↑↑μ {a | f a < c} = 0

case neg
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
H : ¬¬IsLUB (Set.Iio c) c
⊢ ↑↑μ {a | f a < c} = 0
case neg
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
⊢ ↑↑μ {a | f a < c} = 0
by_cases H : ¬IsLUB (Set.Iio c) c
case neg
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
⊢ ↑↑μ {a | f a < c} = 0
case neg
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
H : ¬¬IsLUB (Set.Iio c) c
⊢ ↑↑μ {a | f a < c} = 0
push_neg at H h
case neg.intro.intro.intro.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
⊢ ↑↑μ {a | f a < c} = 0
case neg
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
⊢ ↑↑μ {a | f a < c} = 0
obtain ⟨u, _, u_lt, u_lim, -⟩ :
  ∃ u : ℕ → β,
    StrictMono u ∧ (∀ n : ℕ, u n < c) ∧ Tendsto u atTop (nhds c) ∧ ∀ n : ℕ, u n ∈ Set.Iio c :=
  H.exists_seq_strictMono_tendsto_of_not_mem (lt_irrefl c) h
case neg.intro.intro.intro.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
h_Union : {x | f x < c} = ⋃ (n : ℕ), {x | f x ≤ u n}
⊢ ∀ (i : ℕ), ↑↑μ {x | f x ≤ u i} = 0
case neg.intro.intro.intro.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
h_Union : {x | f x < c} = ⋃ (n : ℕ), {x | f x ≤ u n}
⊢ ↑↑μ {a | f a < c} = 0
rw [h_Union, measure_iUnion_null_iff]
case neg.intro.intro.intro.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
h_Union : {x | f x < c} = ⋃ (n : ℕ), {x | f x ≤ u n}
n : ℕ
⊢ ↑↑μ {x | f x ≤ u n} = 0
case neg.intro.intro.intro.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
h_Union : {x | f x < c} = ⋃ (n : ℕ), {x | f x ≤ u n}
⊢ ∀ (i : ℕ), ↑↑μ {x | f x ≤ u i} = 0
intro n
no goals
case neg.intro.intro.intro.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
h_Union : {x | f x < c} = ⋃ (n : ℕ), {x | f x ≤ u n}
n : ℕ
⊢ ↑↑μ {x | f x ≤ u n} = 0
exact hc _ (u_lt n)
case mp
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
h : ↑↑μ {a | f a < c} = 0
b : β
hb : b < c
⊢ ↑↑μ {x | f x ≤ b} = 0
case mp
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ ↑↑μ {a | f a < c} = 0 → ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
intro h b hb
no goals
case mp
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
h : ↑↑μ {a | f a < c} = 0
b : β
hb : b < c
⊢ ↑↑μ {x | f x ≤ b} = 0
exact measure_mono_null (fun y hy => (lt_of_le_of_lt hy hb : _)) h
case pos
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ∀ (b : β), c ≤ b
this : {a | f a < c} = ∅
⊢ ↑↑μ {a | f a < c} = 0
case pos
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ∀ (b : β), c ≤ b
⊢ ↑↑μ {a | f a < c} = 0
have : {a : α | f a < c} = ∅ := by
  apply Set.eq_empty_iff_forall_not_mem.2 fun x hx => ?_
  exact (lt_irrefl _ (lt_of_lt_of_le hx (h (f x)))).elim
no goals
case pos
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ∀ (b : β), c ≤ b
this : {a | f a < c} = ∅
⊢ ↑↑μ {a | f a < c} = 0
simp [this]
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ∀ (b : β), c ≤ b
x : α
hx : x ∈ {a | f a < c}
⊢ False
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ∀ (b : β), c ≤ b
⊢ {a | f a < c} = ∅
apply Set.eq_empty_iff_forall_not_mem.2 fun x hx => ?_
no goals
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ∀ (b : β), c ≤ b
x : α
hx : x ∈ {a | f a < c}
⊢ False
exact (lt_irrefl _ (lt_of_lt_of_le hx (h (f x)))).elim
case pos
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
H : ¬IsLUB (Set.Iio c) c
this : c ∈ upperBounds (Set.Iio c)
⊢ ↑↑μ {a | f a < c} = 0
case pos
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
H : ¬IsLUB (Set.Iio c) c
⊢ ↑↑μ {a | f a < c} = 0
have : c ∈ upperBounds (Set.Iio c) := fun y hy => le_of_lt hy
case pos.intro.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
H : ¬IsLUB (Set.Iio c) c
this : c ∈ upperBounds (Set.Iio c)
b : β
b_up : b ∈ upperBounds (Set.Iio c)
bc : b < c
⊢ ↑↑μ {a | f a < c} = 0
case pos
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
H : ¬IsLUB (Set.Iio c) c
this : c ∈ upperBounds (Set.Iio c)
⊢ ↑↑μ {a | f a < c} = 0
obtain ⟨b, b_up, bc⟩ : ∃ b : β, b ∈ upperBounds (Set.Iio c) ∧ b < c := by
  simpa [IsLUB, IsLeast, this, lowerBounds] using H
no goals
case pos.intro.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
H : ¬IsLUB (Set.Iio c) c
this : c ∈ upperBounds (Set.Iio c)
b : β
b_up : b ∈ upperBounds (Set.Iio c)
bc : b < c
⊢ ↑↑μ {a | f a < c} = 0
exact measure_mono_null (fun x hx => b_up hx) (hc b bc)
no goals
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
H : ¬IsLUB (Set.Iio c) c
this : c ∈ upperBounds (Set.Iio c)
⊢ ∃ b, b ∈ upperBounds (Set.Iio c) ∧ b < c
simpa [IsLUB, IsLeast, this, lowerBounds] using H
case h
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
⊢ x ∈ {x | f x < c} ↔ x ∈ ⋃ (n : ℕ), {x | f x ≤ u n}
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
⊢ {x | f x < c} = ⋃ (n : ℕ), {x | f x ≤ u n}
ext1 x
case h
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
⊢ f x < c ↔ ∃ i, f x ≤ u i
case h
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
⊢ x ∈ {x | f x < c} ↔ x ∈ ⋃ (n : ℕ), {x | f x ≤ u n}
simp_rw [Set.mem_iUnion, Set.mem_setOf_eq]
case h.mp
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h✝ : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
h : f x < c
⊢ ∃ i, f x ≤ u i

case h.mpr
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h✝ : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
h : ∃ i, f x ≤ u i
⊢ f x < c
case h
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
⊢ f x < c ↔ ∃ i, f x ≤ u i
constructor <;> intro h
case h.mp.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h✝ : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
h : f x < c
n : ℕ
hn : f x < u n
⊢ ∃ i, f x ≤ u i
case h.mp
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h✝ : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
h : f x < c
⊢ ∃ i, f x ≤ u i
obtain ⟨n, hn⟩ := ((tendsto_order.1 u_lim).1 _ h).exists
no goals
case h.mp.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h✝ : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
h : f x < c
n : ℕ
hn : f x < u n
⊢ ∃ i, f x ≤ u i
exact ⟨n, hn.le⟩
case h.mpr.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
n : ℕ
hn : f x ≤ u n
⊢ f x < c
case h.mpr
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h✝ : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
h : ∃ i, f x ≤ u i
⊢ f x < c
obtain ⟨n, hn⟩ := h
no goals
case h.mpr.intro
α : Type u_2
E : Type ?u.30634
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
p : ℝ≥0∞
β : Type u_1
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ (b : β), b < c → ↑↑μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (nhds c)
x : α
n : ℕ
hn : f x ≤ u n
⊢ f x < c
exact hn.trans_lt (u_lt _)