English
If every f(a) is supported on S, then read(dec f) is supported on S.
Русский
Если для каждого a поддержка f(a) на S, тогда поддержка чтения read(dec f) на S.
LaTeX
$$SupportsStmt S (read dec f)$$
Lean4
theorem stmts_supportsStmt {M : Λ → Stmt Γ Λ σ} {S : Finset Λ} {q : Stmt Γ Λ σ} (ss : Supports M S) :
some q ∈ stmts M S → SupportsStmt S q :=
by
simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq, forall_eq',
exists_imp, and_imp]
exact fun l ls h ↦ stmts₁_supportsStmt_mono h (ss.2 _ ls)