mem_εClosure_iff_exists — Mathlib

English

An element s belongs to M.εClosure S if and only if there exists t in S such that s ∈ M.εClosure{t}.

Русский

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

LaTeX

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

Lean4

theorem mem_εClosure_iff_exists : s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure { t }
    where
  mp
    h := by
    induction h with
    | base => tauto
    | step _ _ _ _ ih =>
      obtain ⟨s, _, _⟩ := ih
      use s
      solve_by_elim [εClosure.step]
  mpr := by
    intro ⟨t, _, h⟩
    induction h <;> subst_vars <;> solve_by_elim [εClosure.step]

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