eqOn_or_eventually_ne_of_preconnected

English

Let f and g be analytic on nhds of a preconnected set U. Then either f=g on U, or f≠g on a codiscreteWithin U set (i.e., they differ on a large subset).

Русский

Пусть f,g аналитичны на nhds(U). Тогда либо f=g на U, либо f≠g на существенно большой подмножестве U (codiscreteWithin U).

LaTeX

$$$$\\text{Let } f,g\\text{ be analytic on }U. \\; \\text{Then } f=g \\text{ on }U \\lor \\forall^{\\infty} x\\in\\mathrm{codiscreteWithin}(U),\n f(x)\\neq g(x).$$$$

Lean4

theorem eqOn_or_eventually_ne_of_preconnected (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U)
    (hU : IsPreconnected U) : EqOn f g U ∨ ∀ᶠ x in codiscreteWithin U, f x ≠ g x :=
  (eqOn_zero_or_eventually_ne_zero_of_preconnected (hf.sub hg) hU).imp (fun h _ hx ↦ eq_of_sub_eq_zero (h hx))
    (by simp only [Pi.sub_apply, ne_eq, sub_eq_zero, imp_self])

Похожие утверждения