codeSupp'_self — Mathlib

English

When applying trStmts₁ to a push operation, it equals inserting the push state into trStmts₁ of the original, preserving the structure.

Русский

При применении к операции push к функции trStmts₁ получается добавление состояния push в trStmts₁ исходного, сохраняя структуру.

LaTeX

$$$\\forall k\\; \\forall s\\; \\forall q:\\;\\;\\mathrm{trStmts}_1(\\mathrm{Λ'}.push\\; k\\; s\\; q) = \\mathrm{Finset}.insert(\\mathrm{Λ'}.push\\; k\\; s\\; q)(\\mathrm{trStmts}_1(q))$$$

Lean4

@[simp]
theorem codeSupp'_self (c k) : trStmts₁ (trNormal c k) ⊆ codeSupp' c k := by
  cases c <;>
    first
    | rfl
    | exact Finset.union_subset_left (fun _ a ↦ a)

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