English
If a function is order-theoretically left-continuous between conditionally complete orders with order topology and the domain is densely ordered, then it is topologically left-continuous.
Русский
Если функция слева непрерывна в смысле порядка между частично упорядоченными полноупорядоченными множествами с порядковой топологией, и множество домена densely ordered, то она топологически слева непрерывна.
LaTeX
$$$\text{LeftOrdContinuous}(f) \rightarrow \text{ContinuousWithinAt}(f, Iic(x), x)$$$
Lean4
/-- An order-theoretically left-continuous function is topologically left-continuous, assuming
the function is between conditionally complete linear orders with order topologies, and the domain
is densely ordered. -/
theorem continuousWithinAt_Iic (hf : LeftOrdContinuous f) : ContinuousWithinAt f (Iic x) x :=
by
rw [ContinuousWithinAt, OrderTopology.topology_eq_generate_intervals (α := Y)]
simp_rw [TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_nhdsWithin]
rintro V ⟨z, rfl | rfl⟩ hxz
· obtain ⟨_, ⟨a, hax, rfl⟩, hza⟩ := (lt_isLUB_iff <| hf isLUB_Iio).mp hxz
exact
⟨Ioi a, isOpen_Ioi, hax, fun b hab ↦ hza.trans_le <| hf.mono hab.1.le⟩
-- The case `V = Iio z`.
· exact ⟨univ, isOpen_univ, trivial, fun a ha ↦ (hf.mono ha.2).trans_lt hxz⟩
