lt — Mathlib · SciLib

English

If x is infinitesimally close to r and y is infinitesimally close to s with r < s, then x < y.

Русский

Если x бесконечно близко к r, а y — к s, и r < s, то x < y.

LaTeX

$$$x.IsSt r \\rightarrow y.IsSt s \\rightarrow r < s \\rightarrow x < y$$$

Lean4

protected theorem lt {x y : ℝ*} {r s : ℝ} (hxr : IsSt x r) (hys : IsSt y s) (hrs : r < s) : x < y :=
  by
  rcases ofSeq_surjective x with ⟨f, rfl⟩
  rcases ofSeq_surjective y with ⟨g, rfl⟩
  rw [isSt_ofSeq_iff_tendsto] at hxr hys
  exact ofSeq_lt_ofSeq.2 <| hxr.eventually_lt hys hrs

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