leftQuotient_append — Mathlib

English

For a language L and lists x, y, the left quotient distributes over append: L.leftQuotient (x ++ y) = (L.leftQuotient x).leftQuotient y.

Русский

Для языка L и списков x, y левое частное по конкатенации распределяется: L.leftQuotient (x ++ y) = (L.leftQuotient x).leftQuotient y.

LaTeX

$$$L.leftQuotient (x \\;\\|\\; y) = (L.leftQuotient x).leftQuotient y$$$

Lean4

theorem leftQuotient_append (x y : List α) : L.leftQuotient (x ++ y) = (L.leftQuotient x).leftQuotient y := by
  simp [leftQuotient, Language]

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