A normal function is strictly monotone and continuous #
We defined the predicate Order.IsNormal in terms of IsLUB, which avoids having to import
topology in order theory files. This file shows that the predicate is equivalent to the definition
in the literature, being that of a strictly monotonic function, continuous in the order topology.
theorem
Order.IsNormal.continuous
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[WellFoundedLT α]
[TopologicalSpace α]
[OrderTopology α]
[LinearOrder β]
[WellFoundedLT β]
[TopologicalSpace β]
[OrderTopology β]
{f : α → β}
(hf : IsNormal f)
:
theorem
Order.isNormal_iff_strictMono_and_continuous
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[WellFoundedLT α]
[TopologicalSpace α]
[OrderTopology α]
[LinearOrder β]
[WellFoundedLT β]
[TopologicalSpace β]
[OrderTopology β]
{f : α → β}
:
A normal function between well-orders is equivalent to a strictly monotone, continuous function.