kstar_eq_iSup_pow — Mathlib

English

The Kleene star of a language l is the supremum of all its finite powers: l^* = ⋁_{i∈ℕ} l^i.

Русский

Звёздочка Клейна для языка l равна наименьшей верхней границе всех его конечных степеней: l^* = ⋁_{i∈ℕ} l^i.

LaTeX

$$$l^{\\ast} = \\bigvee_{i \\in \\mathbb{N}} l^{i}$$$

Lean4

theorem kstar_eq_iSup_pow (l : Language α) : l∗ = ⨆ i : ℕ, l ^ i :=
  by
  ext x
  simp only [mem_kstar, mem_iSup, mem_pow]
  grind

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