mem_map_succ_iff — Mathlib

English

Let b ∈ β, v : Vector α (n+1) and f : α → β. Then b ∈ (v.map f).toList iff f (v.head) = b or there exists a ∈ v.tail.toList with f a = b.

Русский

Пусть b ∈ β, v : Vector α (n+1) и f : α → β. Тогда b ∈ (v.map f).toList тогда и только тогда, когда f (v.head) = b или существует a ∈ v.tail.toList такое, что f a = b.

LaTeX

$$$b \in (v.map f).toList \iff f v.head = b \lor \exists a : \alpha, a \in v.tail.toList ∧ f a = b$$$

Lean4

theorem mem_map_succ_iff (b : β) (v : Vector α (n + 1)) (f : α → β) :
    b ∈ (v.map f).toList ↔ f v.head = b ∨ ∃ a : α, a ∈ v.tail.toList ∧ f a = b := by
  rw [mem_succ_iff, head_map, tail_map, mem_map_iff, @eq_comm _ b]

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