α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
⊢ f =ᵐ[μ] 0
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
⊢ f =ᵐ[μ] 0
let s := denseSeq E
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
⊢ f =ᵐ[μ] 0
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
⊢ f =ᵐ[μ] 0
have hs : DenseRange s := denseRange_denseSeq E
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
⊢ f =ᵐ[μ] 0
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
⊢ f =ᵐ[μ] 0
have hf' : ∀ᵐ x ∂μ, ∀ n : ℕ, inner (s n) (f x) = (0 : 𝕜) := ae_all_iff.mpr fun n => hf (s n)
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
⊢ f x = OfNat.ofNat 0 x
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
⊢ f =ᵐ[μ] 0
refine' hf'.mono fun x hx => _
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
⊢ inner (f x) (f x) = 0
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
⊢ f x = OfNat.ofNat 0 x
rw [Pi.zero_apply, ← @inner_self_eq_zero 𝕜]
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
h_closed : IsClosed {c | inner c (f x) = 0}
⊢ inner (f x) (f x) = 0
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
⊢ inner (f x) (f x) = 0
have h_closed : IsClosed {c : E | inner c (f x) = (0 : 𝕜)} :=
  isClosed_eq (continuous_id.inner continuous_const) continuous_const
no goals
α : Type u_3
E : Type u_1
𝕜 : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
h_closed : IsClosed {c | inner c (f x) = 0}
⊢ inner (f x) (f x) = 0
exact @isClosed_property ℕ E _ s (fun c => inner c (f x) = (0 : 𝕜)) hs h_closed (fun n => hx n) _