mem_equiv_left — Mathlib

English

If a ~ a' and a belongs to l, then a' also belongs to l; membership is preserved under equivalence.

Русский

Если a эквивалентно a' и a принадлежит l, то и a' принадлежит l; членство сохраняется под эквивалентностью.

LaTeX

$$$a \\sim a' \\implies (a \\in l \\leftrightarrow a' \\in l)$$$

Lean4

theorem mem_equiv_left {l : Lists' α true} : ∀ {a a'}, a ~ a' → (a ∈ l ↔ a' ∈ l) :=
  suffices ∀ {a a'}, a ~ a' → a ∈ l → a' ∈ l from fun e => ⟨this e, this e.symm⟩
  fun e₁ ⟨_, m₃, e₂⟩ => ⟨_, m₃, e₁.symm.trans e₂⟩

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