E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ f z = f w
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
⊢ f z = f w
set g : ℂ → F := f ∘ fun t : ℂ => t • (w - z) + z
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ g 0 = g 1
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ f z = f w
suffices g 0 = g 1 by simpa
case hf
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ Differentiable ℂ g

case hb
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ Metric.Bounded (range g)
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ g 0 = g 1
apply liouville_theorem_aux
no goals
case hf
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ Differentiable ℂ g

case hb
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
⊢ Metric.Bounded (range g)
exacts [hf.comp ((differentiable_id.smul_const (w - z)).add_const z),
  hb.mono (range_comp_subset_range _ _)]
no goals
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Metric.Bounded (range f)
z w : E
g : ℂ → F := f ∘ fun t => t • (w - z) + z
this : g 0 = g 1
⊢ f z = f w
simpa