English
If contSupp k ⊆ S, then the state contSupp k is S-supported.
Русский
Если contSupp k ⊆ S, то contSupp k поддерживается S.
LaTeX
$$$\\operatorname{contSupp}(k) \\subseteq S \\Rightarrow \\mathrm{Supports}(\\operatorname{contSupp} (k), S).$$$
Lean4
theorem contSupp_supports {S k} (H : contSupp k ⊆ S) : Supports (contSupp k) S := by
induction k with
| halt => simp [contSupp_halt, Supports]
| cons₁ f k IH =>
have H₁ := H; rw [contSupp_cons₁] at H₁; have H₂ := Finset.union_subset_right H₁
refine trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => ?_
refine supports_union.2 ⟨codeSupp'_supports H₂, ?_⟩
simp only [codeSupp, contSupp_cons₂, Finset.union_subset_iff] at H₂
exact trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH
| cons₂ k IH =>
have H' := H; rw [contSupp_cons₂] at H'
exact trStmts₁_supports' (head_supports <| Finset.union_subset_right H') H' IH
| comp f k IH =>
have H' := H; rw [contSupp_comp] at H'; have H₂ := Finset.union_subset_right H'
exact supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩
| fix f k IH =>
rw [contSupp] at H
exact supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩
