English
If a function is order-theoretically right-continuous between conditionally complete orders with order topology and the domain is densely ordered, then it is topologically right-continuous.
Русский
Если функция справа непрерывна в смысле порядка между частично упорядоченными полноупорядоченными множествами с порядковой топологией, и домен плотно упорядочен, то она топологически справа непрерывна.
LaTeX
$$$\text{RightOrdContinuous}(f) \rightarrow \text{ContinuousWithinAt}(f, Ici(x), x)$$$
Lean4
/-- An order-theoretically right-continuous function is topologically right-continuous, assuming
the function is between conditionally complete linear orders with order topologies, and the domain
is densely ordered. -/
theorem continuousWithinAt_Ici (hf : RightOrdContinuous f) : ContinuousWithinAt f (Ici x) x :=
hf.orderDual.continuousWithinAt_Iic
