codeSupp_fix — Mathlib

English

The codeSupp for Code.fix f on k is the union of the trace from trNormal (Code.fix f) k with codeSupp f (Cont'.fix f k).

Русский

Code.fix f на k имеет codeSupp = тр trace from trNormal (Code.fix f) k и codeSupp f (Cont'.fix f k).

LaTeX

$$$\forall f k\; codeSupp (Code.fix f) k = trStmts₁ (trNormal (Code.fix f) k) \cup codeSupp f (Cont'.fix f k)$$$

Lean4

@[simp]
theorem codeSupp_fix (f k) :
    codeSupp (Code.fix f) k = trStmts₁ (trNormal (Code.fix f) k) ∪ codeSupp f (Cont'.fix f k) := by
  simp [codeSupp, codeSupp', contSupp, Finset.union_assoc, Finset.union_left_comm, Finset.union_left_idem]

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