stmts_trans — Mathlib

English

If q1 ∈ stmts₁ q₂, then membership propagates along step translation from q₂ to q₁.

Русский

Если q₁ ∈ stmts₁(q₂), тогда переходная индукция сохраняет принадлежность для q₁ по отношению к q₂.

LaTeX

$$stmts₁_trans (q₁) (q₂) ...$$

Lean4

theorem stmts_trans {M : Λ → Stmt Γ Λ σ} {S : Finset Λ} {q₁ q₂ : Stmt Γ Λ σ} (h₁ : q₁ ∈ stmts₁ q₂) :
    some q₂ ∈ stmts M S → some q₁ ∈ stmts M S :=
  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₂ ↦ ⟨_, ls, stmts₁_trans h₂ h₁⟩

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