mem_cons — Mathlib

English

Let a, y be elements and l a list of Lists α. An element a belongs to the list cons(y, l) if and only if a is equivalent to y or a belongs to l.

Русский

Пусть a, y — элементы, а l — список из элементов Lists α. Элемент a принадлежит списку cons(y, l) тогда и только тогда, когда a эквивалентен y или a принадлежит l.

LaTeX

$$$a \\in \\operatorname{cons}(y,l) \\;\\iff\\; a \\sim y \\;\\lor\\; a \\in l$$$

Lean4

@[simp]
theorem mem_cons {a y l} : a ∈ @cons α y l ↔ a ~ y ∨ a ∈ l := by simp [mem_def, or_and_right, exists_or]

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