Picard's little theorem
Closed
Theorem & proof
·
picard_little.lean
·
✓ verified
1
2
3
import Mathlib theorem picard_little (f : ℂ → ℂ) (hf : Differentiable ℂ f) (h : ¬ ∃ c, ∀ z, f z = c) : ∀ a b : ℂ, a ≠ b → (Set.range f)ᶜ ⊆ {a, b} :=sorry
Rewards pledged
No rewards pledged yet.