mem_evalFrom_iff_exists — Mathlib

English

An element s belongs to M.evalFrom S x iff there exists t ∈ S such that s ∈ M.evalFrom {t} x.

Русский

Элемент s принадлежит M.evalFrom S x тогда и только тогда, когда существует t ∈ S такое, что s ∈ M.evalFrom{t} x.

LaTeX

$$$s \in M.\\evalFrom S x \\Leftrightarrow \\exists t \in S, s \in M.\\evalFrom\{t\} x$$$

Lean4

theorem mem_evalFrom_iff_exists {s : σ} {S : Set σ} {x : List α} :
    s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom { t } x := by
  induction x using List.reverseRecOn generalizing s with
  | nil => apply mem_εClosure_iff_exists
  | append_singleton _ _ ih =>
    simp_rw [evalFrom_append_singleton, mem_stepSet_iff, ih]
    tauto

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