codeSupp_cons — Mathlib

English

If q' is a member of trStmts₁ q then trStmts₁ q' is a subset of trStmts₁ q.

Русский

Если q' принадлежит trStmts₁ q, то trStmts₁ q' ⊆ trStmts₁ q.

LaTeX

$$$\forall q q'$, if $q' \in trStmts₁ q$ then $trStmts₁ q' \subseteq trStmts₁ q$$$

Lean4

@[simp]
theorem codeSupp_cons (f fs k) :
    codeSupp (Code.cons f fs) k = trStmts₁ (trNormal (Code.cons f fs) k) ∪ codeSupp f (Cont'.cons₁ fs k) := by
  simp [codeSupp, codeSupp', contSupp, Finset.union_assoc]

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