stmts_trans — Mathlib

English

If q1 ∈ stmts1(q2) and q2 ∈ stmts(M,S), then q1 ∈ stmts(M,S).

Русский

Если q1 ∈ stmts1(q2) и q2 ∈ stmts(M,S), то q1 ∈ stmts(M,S).

LaTeX

$$$ q_1 \in stmts_1(q_2) \Rightarrow q_2 \in stmts(M,S) \Rightarrow q_1 \in stmts(M,S) $$$

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₁⟩

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