stmts_supportsStmt — Mathlib

English

If S supports all statements in stmts(M,S), then it also supports any statement in stmts(M,S) that is produced by stepping.

Русский

Если S поддерживает все инструкции в stmts(M,S), то она поддерживает и любое q, полученное в ходе шага.

LaTeX

$$$ \forall q' \in stmts(M,S),\; SupportsStmt S q' \,\text{(из шага)} $$$

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)

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