duplicate_cons_iff — Mathlib

English

For any x, y, l, x is duplicated in y :: l exactly when either y = x and x ∈ l, or x is already duplicated in l.

Русский

Для любых x, y, l элемент x дублируется в y :: l тогда и только тогда, когда либо y = x и x ∈ l, либо x уже дублируется в l.

LaTeX

$$$ x \in+ y \:::\: l \iff (y = x \land x \in l) \lor x \in+ l $$$

Lean4

theorem duplicate_cons_iff {y : α} : x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l :=
  by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · obtain hm | hm := h
    · exact Or.inl ⟨rfl, hm⟩
    · exact Or.inr hm
  · rcases h with (⟨rfl | h⟩ | h)
    · simpa
    · exact h.cons_duplicate

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