le_iff_deriv — Mathlib

English

For a normal f, f a ≤ a iff there exists o with deriv f o = a.

Русский

Для нормальной f выполняется: f a ≤ a тогда и только если существует o, такое что deriv f o = a.

LaTeX

$$$$ f a \le a \iff \exists o, \operatorname{deriv} f o = a $$$$

Lean4

theorem le_iff_deriv (H : IsNormal f) {a} : f a ≤ a ↔ ∃ o, deriv f o = a :=
  by
  unfold deriv
  rw [← le_iff_derivFamily fun _ : Unit => H]
  exact ⟨fun h _ => h, fun h => h Unit.unit⟩

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