exists_eq_const_of_bounded — Mathlib

English

There exists c with f = const E c when f is differentiable and bounded.

Русский

Пусть f дифференцируема и ограничена; существует константа c такой, что f = const E c.

LaTeX

$$$\\exists c, f = \\text{const } E c$$$

Lean4

/-- **Liouville's theorem**: a complex differentiable bounded function is a constant. -/
theorem exists_eq_const_of_bounded {f : E → F} (hf : Differentiable ℂ f) (hb : IsBounded (range f)) :
    ∃ c, f = const E c :=
  (hf.exists_const_forall_eq_of_bounded hb).imp fun _ => funext

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