deriv_limit — Mathlib

English

If o is a succ-limit ordinal, then deriv f o equals the supremum of deriv f a over all a < o.

Русский

Если o является предельным порядком типа succ, то deriv f o равна надполу произведения deriv f a по всем a < o.

LaTeX

$$$$ \operatorname{IsSuccLimit}(o) \Rightarrow \operatorname{deriv} f o = \bigvee_{a : \{ a \mid a < o \}} \operatorname{deriv} f a $$$$

Lean4

theorem deriv_limit (f) {o} : IsSuccLimit o → deriv f o = ⨆ a : { a // a < o }, deriv f a :=
  derivFamily_limit _

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