codeSupp_comp — Mathlib

English

For any q₁, q₂, q′, we have the property that trStmts₁ (q₁.pred q₂) equals an insertion of q₁.pred q₂ into the union of trStmts₁ q₁ and trStmts₁ q₂.

Русский

Для любых q₁, q₂, q′ равенство trStmts₁ (q₁.pred q₂) = вставка q₁.pred q₂ в объединение trStmts₁ q₁ и trStmts₁ q₂.

LaTeX

$$$\forall (q_1 q_2 : Λ'),\\; trStmts₁ (q_1.pred q_2) = \\text{insert}(q_1.pred q_2, trStmts₁(q_1) \cup trStmts₁(q_2))$$$

Lean4

@[simp]
theorem codeSupp_comp (f g k) :
    codeSupp (Code.comp f g) k = trStmts₁ (trNormal (Code.comp f g) k) ∪ codeSupp g (Cont'.comp f k) :=
  by
  simp only [codeSupp, codeSupp', trNormal, Finset.union_assoc, contSupp]
  rw [← Finset.union_assoc _ _ (contSupp k), Finset.union_eq_right.2 (codeSupp'_self _ _)]

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