deriv_char_of_ne — Mathlib

English

If a ≠ b, the derivative of the single-character regex char a with respect to b is the empty regex (0).

Русский

Если a ≠ b, производная по символу у регулярного выражения char a относительно b равна пустому выражению 0.

LaTeX

$$$$ a \\neq b \\implies \\mathrm{deriv}(\\mathrm{char}(a), b) = 0. $$$$

Lean4

@[simp]
theorem deriv_char_of_ne (h : a ≠ b) : deriv (char a) b = 0 :=
  if_neg h

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