mem_stepSet_iff — Mathlib

English

An element s belongs to M.stepSet S a if and only if there exists t in S such that s ∈ εClosure(M.step t a).

Русский

s ∈ M.stepSet S a тогда и только тогда, когда существует t ∈ S с s ∈ εClosure(M.step t a).

LaTeX

$$$s \in M.stepSet S a \Leftrightarrow \exists t \in S, s \in M.\\varepsilonClosure( M.\\step t a )$$$

Lean4

@[simp]
theorem mem_stepSet_iff : s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t a) := by
  simp_rw [stepSet, mem_iUnion₂, exists_prop]

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