English
Let α be a linearly ordered topological space with order-closed topology. If f, g : γ → α have limits y and z along a filter l with y < z, then eventually f(x) < g(x) along l.
Русский
Пусть α — линейно упорядоченное топологическое пространство с Order-Closed топологией. Пусть f, g : γ → α имеют пределы y и z вдоль фильтра l с условием y < z. Тогда почти всюду (для больших элементов) выполняется f(x) < g(x).
LaTeX
$$$(\operatorname{Tendsto} f\ l\ (\mathcal{N} y)) \land (\operatorname{Tendsto} g\ l\ (\mathcal{N} z)) \land y < z \Rightarrow \forall^\infty x \in l,\ f(x) < g(x).$$$
Lean4
theorem eventually_lt {l : Filter γ} {f g : γ → α} {y z : α} (hf : Tendsto f l (𝓝 y)) (hg : Tendsto g l (𝓝 z))
(hyz : y < z) : ∀ᶠ x in l, f x < g x :=
let ⟨_a, ha, _b, hb, h⟩ := hyz.exists_disjoint_Iio_Ioi
(hg.eventually (Ioi_mem_nhds hb)).mp <| (hf.eventually (Iio_mem_nhds ha)).mono fun _ h₁ h₂ => h _ h₁ _ h₂
