derivFamily_strictMono — Mathlib

English

If the index set ι is small, then the derivative family derivFamily f is strictly increasing.

Русский

Если множество индексов ι является малым, то производная семейства derivFamily f строго возрастает.

LaTeX

$$$$ StrictMono(derivFamily f). $$$$

Lean4

theorem derivFamily_strictMono [Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) : StrictMono (derivFamily f) :=
  (isNormal_derivFamily f).strictMono

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