English
Arden's lemma: If ε ∉ m, then the solution of l = m·l + n is equivalent to l = m^* n; in particular, l = m^* n if and only if l = m·l + n (under the usual condition).
Русский
Лемма Ардена: если ε не принадлежит m, то решение уравнения l = m·l + n эквивалентно l = m^* n; то есть l = m^* n тогда и только тогда, когда l = m·l + n (при условии).
LaTeX
$$$(\\varepsilon \\notin m) \\;\\rightarrow\\; [\, l = m \\cdot l + n \\;\\Leftrightarrow\\; l = m^{\\ast} \\cdot n \]$$$
Lean4
/-- **Arden's lemma** -/
theorem self_eq_mul_add_iff {l m n : Language α} (hm : [] ∉ m) : l = m * l + n ↔ l = m∗ * n
where
mp
h := by
apply le_antisymm
· intro x hx
induction hlen : x.length using Nat.strong_induction_on generalizing x with
| _ _ ih
subst hlen
rw [h] at hx
obtain hx | hx := hx
· obtain ⟨a, ha, b, hb, rfl⟩ := mem_mul.mp hx
rw [length_append] at ih
have hal : 0 < a.length := length_pos_iff.mpr <| ne_of_mem_of_not_mem ha hm
specialize ih b.length (Nat.lt_add_left_iff_pos.mpr hal) hb rfl
rw [← one_add_self_mul_kstar_eq_kstar, one_add_mul, mul_assoc]
right
exact ⟨_, ha, _, ih, rfl⟩
· exact ⟨[], nil_mem_kstar _, _, ⟨hx, nil_append _⟩⟩
· rw [kstar_eq_iSup_pow, iSup_mul, iSup_le_iff]
intro i
induction i with rw [h]
| zero =>
rw [pow_zero, one_mul, add_comm]
exact le_self_add
| succ _ ih =>
rw [add_comm, pow_add, pow_one, mul_assoc]
exact le_add_right (mul_le_mul_left' ih _)
mpr h := by rw [h, add_comm, ← mul_assoc, ← one_add_mul, one_add_self_mul_kstar_eq_kstar]
