seqTendstoAeSeq_strictMono — Mathlib

English

The function seqTendstoAeSeq is strictly monotone in its argument when hfg holds.

Русский

Функция seqTendstoAeSeq строго возрастает по аргументу при выполнении условия hfg.

LaTeX

$$$\text{If } hfg,\; \text{then } \text{StrictMono}(seqTendstoAeSeq(hfg)).$$$

Lean4

theorem seqTendstoAeSeq_strictMono (hfg : TendstoInMeasure μ f atTop g) : StrictMono (seqTendstoAeSeq hfg) :=
  by
  refine strictMono_nat_of_lt_succ fun n => ?_
  rw [seqTendstoAeSeq_succ]
  exact lt_of_lt_of_le (lt_add_one <| seqTendstoAeSeq hfg n) (le_max_right _ _)

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