stepSet — Mathlib

English

The one-step set of results from S on input a is the union over all s in S of their one-step sets.

Русский

Объединение состояний, достижимых за один шаг от любого элемента множества S под вход a, равно объединению состояний M.step s a по всем s∈S.

LaTeX

$$$M.stepSet(S,a) = \bigcup_{s \in S} M.step(s,a)$$$

Lean4

/-- `M.stepSet S a` is the union of `M.step s a` for all `s ∈ S`. -/
def stepSet (S : Set σ) (a : α) : Set σ :=
  ⋃ s ∈ S, M.step s a

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