duplicate_cons_iff_of_ne

Mathlib.Data.List.Duplicate

URI: https://scilib.ai/kg/mathlib#List.duplicate_cons_iff_of_ne

English

If x ≠ y, then x ∈+ y :: l is equivalent to x ∈+ l.

Русский

Если x ≠ y, тогда x ∈+ y :: l эквивалентно x ∈+ l.

LaTeX

$$$ x \in+ y \:::\: l \iff x \in+ l \quad (\text{when } x \neq y)$$$

Lean4

theorem duplicate_cons_iff_of_ne {y : α} (hne : x ≠ y) : x ∈+ y :: l ↔ x ∈+ l := by simp [duplicate_cons_iff, hne.symm]

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

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

Разделы

Аффилиация

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