supConvergenceClass — Mathlib

English

A linear ordered space with order topology has SupConvergenceClass.

Русский

Линейно упорядованное пространство с топологией порядка обладает SupConvergenceClass.

LaTeX

$$$\\text{SupConvergenceClass}(\\alpha)$ для линейного порядка $\\alpha$.$$

Lean4

instance (priority := 100) supConvergenceClass [TopologicalSpace α] [LinearOrder α] [OrderTopology α] :
    SupConvergenceClass α :=
  by
  refine ⟨fun a s ha => tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩⟩
  · rcases ha.exists_between hb with ⟨c, hcs, bc, bca⟩
    lift c to s using hcs
    exact (eventually_ge_atTop c).mono fun x hx => bc.trans_le hx
  · exact Eventually.of_forall fun x => (ha.1 x.2).trans_lt hb

Похожие утверждения