stmts_supportsStmt — Mathlib

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)

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