finite_range_leftQuotient — Mathlib

English

If a language L is regular, then the family of its left quotients, i.e. the set { w⁻¹L : w ∈ α* }, is finite.

Русский

Если язык L является регулярным, то множество его левых делителей, то есть { w⁻¹L : w ∈ α* }, конечно.

LaTeX

$$(Set.range L.leftQuotient).Finite → L.IsRegular.$$

Lean4

theorem finite_range_leftQuotient (h : L.IsRegular) : (Set.range L.leftQuotient).Finite :=
  by
  have ⟨σ, x, M, hM⟩ := h
  rw [← hM, leftQuotient_accepts]
  exact Set.finite_of_finite_preimage (Set.toFinite _) (Set.range_comp_subset_range M.eval M.acceptsFrom)

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