mem_iff_get — Mathlib

English

For any vector v, an element a belongs to v.toList if and only if there exists an index i with v.get i = a.

Русский

Для любого вектора v элемент a принадлежит v.toList тогда и только тогда, когда существует индекс i, такой что v.get i = a.

LaTeX

$$$$ a \in v.toList \iff \exists i, v.get i = a $$$$

Lean4

theorem mem_iff_get (v : Vector α n) : a ∈ v.toList ↔ ∃ i, v.get i = a :=
  by
  simp only [List.mem_iff_get, Fin.exists_iff, Vector.get_eq_get_toList]
  exact ⟨fun ⟨i, hi, h⟩ => ⟨i, by rwa [toList_length] at hi, h⟩, fun ⟨i, hi, h⟩ => ⟨i, by rwa [toList_length], h⟩⟩

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