Mathlib v3 is deprecated. Go to Mathlib v4

Theorem differentiable.exists_eq_const_of_bounded

Modification history

2022-02-27 21:28
src/analysis/complex/liouville.lean
feat(analysis/complex/liouville): prove Liouville's theorem (#12095)
Added differentiable.exists_eq_const_of_boundedView on Github →