isWeaklyRegular_singleton_iff — Mathlib

English

A single-element list [r] is weakly regular on M iff r is regular on M.

Русский

Одинарный список [r] слабo регулярен на M тогда и только тогда, когда r регулярна на M.

LaTeX

$$$IsWeaklyRegular(M, [r]) \\iff IsSMulRegular(M, r)$$$

Lean4

theorem isWeaklyRegular_singleton_iff (r : R) : IsWeaklyRegular M [r] ↔ IsSMulRegular M r :=
  Iff.trans (isWeaklyRegular_cons_iff M r []) (and_iff_left (.nil R _))

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