codeSupp_case — Mathlib

English

The codeSupp for Code.case f g k equals the union of the trace from trNormal (Code.case f g) k with the unions codeSupp f k and codeSupp g k.

Русский

Code.case f g k имеет codeSupp, равный объединению следа от trNormal (Code.case f g) k и объединений codeSupp f k и codeSupp g k.

LaTeX

$$$\forall f,g,k\; codeSupp (Code.case f g) k =\; trStmts₁ (trNormal (Code.case f g) k) \cup (codeSupp f k \cup codeSupp g k)$$$

Lean4

@[simp]
theorem codeSupp_case (f g k) :
    codeSupp (Code.case f g) k = trStmts₁ (trNormal (Code.case f g) k) ∪ (codeSupp f k ∪ codeSupp g k) := by
  simp [codeSupp, codeSupp', Finset.union_assoc, Finset.union_left_comm]

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