mem_iff_exists_get? — Mathlib

English

An element x is in s iff there exists i with s.get? i = some x.

Русский

Элемент x принадлежит s тогда и только тогда, когда существует индекс i Such that s.get? i = some x.

LaTeX

$$$x \\in s \\iff \\exists i, s.get? i = \\mathrm{some}(x)$$$

Lean4

theorem mem_iff_exists_get? {s : Seq α} {x : α} : x ∈ s ↔ ∃ i, some x = s.get? i
    where
  mp
    h := by
    change (some x ∈ s.1) at h
    rwa [Stream'.mem_iff_exists_get_eq] at h
  mpr h := get?_mem h.choose_spec.symm

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