trStmts₁_supports' — Mathlib

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⟩

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