one_add_self_mul_kstar_eq_kstar — Mathlib

English

One more than the product of a language with its Kleene star equals the Kleene star: 1 + l · l^* = l^*.

Русский

Ещё на единицу больше произведения языка и его звёздочки равно звёздочке: 1 + l · l^* = l^*.

LaTeX

$$1 + l \\cdot l^{\\ast} = l^{\\ast}$$

Lean4

@[simp]
theorem one_add_self_mul_kstar_eq_kstar (l : Language α) : 1 + l * l∗ = l∗ :=
  by
  simp only [kstar_eq_iSup_pow, mul_iSup, ← pow_succ', ← pow_zero l]
  exact sup_iSup_nat_succ _

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