get?_mem

Mathlib.Data.Seq.Defs

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.get?_mem

English

If s.get? n = some x, then x is an element of s.

Русский

Если s.get? n = some x, то x ∈ s.

LaTeX

$$$\\text{get?}(s,n) = \\mathrm{some}(x) \\Rightarrow x \\in s$$$

Lean4

theorem get?_mem {s : Seq α} {n : ℕ} {x : α} (h : s.get? n = .some x) : x ∈ s :=
  ⟨n, h.symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru