strict_mono — Mathlib

English

If f is a fundamental sequence, then it is monotone: increasing index preserves order.

Русский

Если f — фундаментальная последовательность, то она монотонна: при возрастании индекса сохраняется порядок.

LaTeX

$$$$\text{IsFundamentalSequence}(a,o,f) \Rightarrow \forall i

Lean4

protected theorem strict_mono (hf : IsFundamentalSequence a o f) {i j} : ∀ hi hj, i < j → f i hi < f j hj :=
  hf.2.1

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