mk_mem_sym2 — Mathlib

English

If a and b belong to xs, then s(a,b) belongs to xs.sym2.

Русский

Если a и b принадлежат xs, то s(a,b) принадлежит xs.sym2.

LaTeX

$$$$ a \\in xs \\wedge b \\in xs \\Rightarrow s(a,b) \\in xs.sym2 $$$$

Lean4

theorem mk_mem_sym2 {xs : List α} {a b : α} (ha : a ∈ xs) (hb : b ∈ xs) : s(a, b) ∈ xs.sym2 := by
  induction xs with
  | nil => simp at ha
  | cons x xs ih =>
    rw [mem_sym2_cons_iff]
    rw [mem_cons] at ha hb
    obtain (rfl | ha) := ha <;> obtain (rfl | hb) := hb
    · left; rfl
    · right; left; use b
    · right; left; rw [Sym2.eq_swap]; use a
    · right; right; exact ih ha hb

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