case pos
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : μ = 0
⊢ AEMeasurable g

case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
⊢ AEMeasurable g
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
⊢ AEMeasurable g
by_cases hμ : μ = 0
case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
⊢ AEMeasurable g
case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
⊢ AEMeasurable g
have : μ.ae.NeBot := by simpa [neBot_iff]
case pos
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : Nonempty ι
⊢ AEMeasurable g

case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
⊢ AEMeasurable g
case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
⊢ AEMeasurable g
by_cases hι : Nonempty ι
case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
⊢ ∃ x, g =ᵐ[μ] fun x_1 => g x
case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
⊢ AEMeasurable g
suffices ∃ x, g =ᵐ[μ] fun _ => g x by
  exact ⟨fun _ => g this.choose, measurable_const, this.choose_spec⟩
case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
h_empty : ∀ (x : δ), {a | ∃ i, f i x = a} = ∅
⊢ ∃ x, g =ᵐ[μ] fun x_1 => g x
case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
⊢ ∃ x, g =ᵐ[μ] fun x_1 => g x
have h_empty : ∀ x, { a : α | ∃ i : ι, f i x = a } = ∅ := by
  intro x
  ext1 y
  rw [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false_iff]
  exact fun hi => hι (nonempty_of_exists hi)
case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
h_empty : ∀ (x : δ), {a | ∃ i, f i x = a} = ∅
hg : ∀ᵐ (b : δ) ∂μ, IsLUB ∅ (g b)
⊢ ∃ x, g =ᵐ[μ] fun x_1 => g x
case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
h_empty : ∀ (x : δ), {a | ∃ i, f i x = a} = ∅
⊢ ∃ x, g =ᵐ[μ] fun x_1 => g x
simp_rw [h_empty] at hg
no goals
case neg
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
h_empty : ∀ (x : δ), {a | ∃ i, f i x = a} = ∅
hg : ∀ᵐ (b : δ) ∂μ, IsLUB ∅ (g b)
⊢ ∃ x, g =ᵐ[μ] fun x_1 => g x
exact ⟨hg.exists.choose, hg.mono fun y hy => IsLUB.unique hy hg.exists.choose_spec⟩
case pos
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : μ = 0
⊢ AEMeasurable g
case pos
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : μ = 0
⊢ AEMeasurable g
rw [hμ]
no goals
case pos
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : μ = 0
⊢ AEMeasurable g
exact aemeasurable_zero_measure
no goals
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
⊢ NeBot (Measure.ae μ)
simpa [neBot_iff]
no goals
case pos
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : Nonempty ι
⊢ AEMeasurable g
exact AEMeasurable.is_lub_of_nonempty hι hf hg
no goals
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
this : ∃ x, g =ᵐ[μ] fun x_1 => g x
⊢ AEMeasurable g
exact ⟨fun _ => g this.choose, measurable_const, this.choose_spec⟩
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
x : δ
⊢ {a | ∃ i, f i x = a} = ∅
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
⊢ ∀ (x : δ), {a | ∃ i, f i x = a} = ∅
intro x
case h
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
x : δ
y : α
⊢ y ∈ {a | ∃ i, f i x = a} ↔ y ∈ ∅
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
x : δ
⊢ {a | ∃ i, f i x = a} = ∅
ext1 y
case h
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
x : δ
y : α
⊢ ¬∃ i, f i x = y
case h
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
x : δ
y : α
⊢ y ∈ {a | ∃ i, f i x = a} ↔ y ∈ ∅
rw [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false_iff]
no goals
case h
α : Type u_3
β : Type ?u.1154773
γ : Type ?u.1154776
γ₂ : Type ?u.1154779
δ : Type u_2
ι✝ : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : BorelSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_1
μ : MeasureTheory.Measure δ
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), AEMeasurable (f i)
hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a | ∃ i, f i b = a} (g b)
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hι : ¬Nonempty ι
x : δ
y : α
⊢ ¬∃ i, f i x = y
exact fun hi => hι (nonempty_of_exists hi)