Monotonicity of transition maps #
A transition map between interval charts, restricted to (the image of) a component of the
overlap, is continuous and injective on an open interval of ℝ≥0, hence strictly
monotone or strictly antitone; and a strictly monotone map of one open interval onto
another sends ends to ends.
theorem
OneMfld.strictMonoOn_or_strictAntiOn_of_injOn_Ioo
{p v : NNReal}
{f : NNReal → NNReal}
(hc : ContinuousOn f (Set.Ioo p v))
(hi : Set.InjOn f (Set.Ioo p v))
:
A continuous injective function on an open interval of ℝ≥0 is strictly monotone or
strictly antitone there.
theorem
OneMfld.tendsto_top_of_strictMonoOn_image
{p v q w : NNReal}
(hpv : p < v)
{f : NNReal → NNReal}
(hm : StrictMonoOn f (Set.Ioo p v))
(himg : f '' Set.Ioo p v = Set.Ioo q w)
:
Filter.Tendsto f (nhdsWithin v (Set.Iio v)) (nhds w)
A strictly monotone map of Ioo p v onto Ioo q w tends to w at the top end.
theorem
OneMfld.tendsto_bot_of_strictMonoOn_image
{p v q w : NNReal}
(hpv : p < v)
{f : NNReal → NNReal}
(hm : StrictMonoOn f (Set.Ioo p v))
(himg : f '' Set.Ioo p v = Set.Ioo q w)
:
Filter.Tendsto f (nhdsWithin p (Set.Ioi p)) (nhds q)
A strictly monotone map of Ioo p v onto Ioo q w tends to q at the bottom end.