exists_const_forall_eq_of_bounded

English

There exists c such that f ≡ c on its domain if f is differentiable and bounded.

Русский

Существуют c, такие что f(z)=c для всех z, если f дифференцируема и ограничена.

LaTeX

$$$\\exists c, \\forall z, f(z)=c$$$

Lean4

/-- **Liouville's theorem**: a complex differentiable bounded function is a constant. -/
theorem exists_const_forall_eq_of_bounded {f : E → F} (hf : Differentiable ℂ f) (hb : IsBounded (range f)) :
    ∃ c, ∀ z, f z = c :=
  ⟨f 0, fun _ => hf.apply_eq_apply_of_bounded hb _ _⟩

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