English
If codeSupp c k ⊆ S, then the normalized trace trNormal c k is S-supported.
Русский
Если codeSupp c k ⊆ S, то trNormal c k поддерживается S.
LaTeX
$$$\\mathrm{codeSupp}(c,k) \\subseteq S \\Rightarrow \\mathrm{Supports}(\\mathrm{trNormal}(c,k), S).$$$
Lean4
theorem trNormal_supports {S c k} (Hk : codeSupp c k ⊆ S) : (trNormal c k).Supports S := by
induction c generalizing k with simp [Λ'.Supports, head]
| zero' => exact Finset.union_subset_right Hk
| succ => intro; split_ifs <;> exact Finset.union_subset_right Hk
| tail => exact Finset.union_subset_right Hk
| cons f fs IHf _ =>
apply IHf
rw [codeSupp_cons] at Hk
exact Finset.union_subset_right Hk
| comp f g _ IHg => apply IHg; rw [codeSupp_comp] at Hk; exact Finset.union_subset_right Hk
| case f g IHf IHg =>
simp only [codeSupp_case, Finset.union_subset_iff] at Hk
exact ⟨IHf Hk.2.1, IHg Hk.2.2⟩
| fix f IHf => apply IHf; rw [codeSupp_fix] at Hk; exact Finset.union_subset_right Hk
