English
If A,B form NoZeroSmulDivisors and f,g are analytic on a nhds of a preconnected U and f(z)·g(z)=0 for all z ∈ U, then either f≡0 on U or g≡0 on U.
Русский
Если A,B удовлетворяют NoZeroSmulDivisors и f,g аналитичны на nhds(U) и f(z)·g(z)=0 для всех z∈U, то либо f≡0 на U, либо g≡0 на U.
LaTeX
$$$$\\forall z\\in U:\\; f(z)\\,\\cdot\, g(z)=0 \\Rightarrow (\\forall z\\in U, f(z)=0) \\lor (\\forall z\\in U, g(z)=0).$$$$
Lean4
/-- If `f, g` are analytic on a neighbourhood of the preconnected open set `U`, and `f • g = 0`
on `U`, then either `f = 0` on `U` or `g = 0` on `U`. -/
theorem eq_zero_or_eq_zero_of_smul_eq_zero [NoZeroSMulDivisors A B] {f : 𝕜 → A} {g : 𝕜 → B} (hf : AnalyticOnNhd 𝕜 f U)
(hg : AnalyticOnNhd 𝕜 g U) (hfg : ∀ z ∈ U, f z • g z = 0) (hU : IsPreconnected U) :
(∀ z ∈ U, f z = 0) ∨ (∀ z ∈ U, g z = 0) := by
-- We want to apply `IsPreconnected.preperfect_of_nontrivial` which requires `U` to have at least
-- two elements. So we need to dispose of the cases `#U = 0` and `#U = 1` first.
by_cases hU' : U = ∅
· simp [hU']
obtain ⟨z, hz⟩ : ∃ z, z ∈ U := nonempty_iff_ne_empty.mpr hU'
by_cases hU'' : U = { z }
· simpa [hU''] using hfg z hz
apply(nontrivial_iff_ne_singleton hz).mpr at hU''
have : ∃ᶠ w in 𝓝[≠] z, w ∈ U := frequently_mem_iff_neBot.mpr <| hU.preperfect_of_nontrivial hU'' z hz
have : ∃ᶠ w in 𝓝[≠] z, f w = 0 ∨ g w = 0 := this.mp <| by filter_upwards with w hw using smul_eq_zero.mp (hfg w hw)
cases frequently_or_distrib.mp this with
| inl h => exact Or.inl <| hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h
| inr h => exact Or.inr <| hg.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h
