mem_evalFrom_iff_exists — Mathlib

English

Membership of a state in M.evalFrom S x is equivalent to the existence of a starting element t in S such that the state belongs to M.evalFrom {t} x.

Русский

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

LaTeX

$$s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ 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
  rw [evalFrom_eq_biUnion_singleton]
  simp

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