mem_pair — Mathlib

English

An element belongs to the two-element list [b,c] iff it equals b or equals c.

Русский

Элемент принадлежит списку [b,c] тогда и только тогда, когда он равен b или равен c.

LaTeX

$$a ∈ [b,c] ⇔ (a = b) ∨ (a = c)$$

Lean4

theorem mem_pair {a b c : α} : a ∈ [b, c] ↔ a = b ∨ a = c := by
  rw [mem_cons, mem_singleton]
    -- The simpNF linter says that the LHS can be simplified via `List.mem_map`.
    -- However this is a higher priority lemma.
    -- It seems the side condition `hf` is not applied by `simpNF`.
    -- https://github.com/leanprover/std4/issues/207

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