English
If q is S-supported, and trStmts₁ q ∪ K ⊆ S, and K ⊆ S → Supports(K,S), then trStmts₁ q ∪ K is S-supported.
Русский
Если q поддерживается S, и trStmts₁ q ∪ K ⊆ S, и K ⊆ S ⇒ Supports(K,S), тогда trStmts₁ q ∪ K поддерживается S.
LaTeX
$$$\\text{If } (q:S) \\text{ is S-supported and } trStmts₁ q \\cup K \\subseteq S \\text{ and } K \\subseteq S \\rightarrow \\mathrm{Supports}(K,S), \\text{ then } \\mathrm{Supports}(trStmts₁ q \\cup K, S).$$$
Lean4
theorem trStmts₁_supports' {S q K} (H₁ : (q : Λ').Supports S) (H₂ : trStmts₁ q ∪ K ⊆ S) (H₃ : K ⊆ S → Supports K S) :
Supports (trStmts₁ q ∪ K) S := by
simp only [Finset.union_subset_iff] at H₂
exact supports_union.2 ⟨trStmts₁_supports H₁ H₂.1, H₃ H₂.2⟩