mem_rcons_iff — Mathlib

English

For p = (i, head) ∈ Pair M i and m ∈ M j, membership ⟨_, m⟩ ∈ (rcons p).toList holds iff ⟨_, m⟩ ∈ p.tail.toList or (m ≠ 1 and ∃ h: i = j, m = h ▸ head).

Русский

Для p = (i, head) ∈ Pair M i и m ∈ M j, принадлежность ⟨_, m⟩ к списку (rcons p).toList эквивалентна либо ⟨_, m⟩ ∈ p.tail.toList, либо m ≠ 1 и существует h: i = j such that m = h ▸ head.

LaTeX

$$$⟨_, m⟩ ∈ (\\mathrm{rcons}(p)).toList \\iff ⟨_, m⟩ ∈ p.tail.toList \\lor (m \\neq 1 \\land (\\exists h : i = j, m = h \\;▸\\; p.head))$$$

Lean4

theorem mem_rcons_iff {i j : ι} (p : Pair M i) (m : M j) :
    ⟨_, m⟩ ∈ (rcons p).toList ↔ ⟨_, m⟩ ∈ p.tail.toList ∨ m ≠ 1 ∧ (∃ h : i = j, m = h ▸ p.head) :=
  by
  simp only [rcons, cons, ne_eq]
  grind

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