seqTendstoAeSeq_succ — Mathlib

English

Relates the (n+1)-st value of the auxiliary subsequence to the maxima of two bounds, used to enforce monotonic growth.

Русский

Связь (n+1)-го элемента вспомогательной подпоследовательности с максимумами двух ограничений, необходимая для обеспечения монотонного роста.

LaTeX

$$$\text{For } hfg,\; seqTendstoAeSeq(hfg)(n+1) = \max( seqTendstoAeSeqAux(hfg)(n+1)) , seqTendstoAeSeq(hfg)(n) + 1)$$$

Lean4

theorem seqTendstoAeSeq_succ (hfg : TendstoInMeasure μ f atTop g) {n : ℕ} :
    seqTendstoAeSeq hfg (n + 1) = max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1) := by
  rw [seqTendstoAeSeq]

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