add_rmatch_iff — Mathlib

English

For regular expressions P and Q, (P + Q).rmatch x is true iff P.rmatch x or Q.rmatch x is true.

Русский

Для регулярных выражений P и Q: (P + Q).rmatch x истинно тогда и только тогда, когда P.rmatch x или Q.rmatch x истинно.

LaTeX

$$$$ (P + Q).rmatch x \\text{ holds } \\iff P.rmatch x \\text{ or } Q.rmatch x. $$$$

Lean4

theorem add_rmatch_iff (P Q : RegularExpression α) (x : List α) : (P + Q).rmatch x ↔ P.rmatch x ∨ Q.rmatch x := by
  induction x generalizing P Q with
  | nil => simp only [rmatch, matchEpsilon, Bool.or_eq_true_iff]
  | cons _ _ ih =>
    rw [rmatch, deriv_add]
    exact ih _ _

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