mem_stepSet — Mathlib

English

A state s belongs to M.stepSet S a if and only if there exists t in S with s in M.step t a.

Русский

Элемент s принадлежит M.stepSet S a тогда и только тогда, когда существует t∈S, такой что s ∈ M.step t a.

LaTeX

$$$s ∈ M.stepSet S a \iff \exists t \in S,\; s \in M.step t a$$$

Lean4

theorem mem_stepSet {s : σ} {S : Set σ} {a : α} : s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.step t a := by simp [stepSet]

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