mk_mem_sym2_iff — Mathlib

English

s(a,b) ∈ xs.sym2 iff a ∈ xs and b ∈ xs.

Русский

s(a,b) ∈ xs.sym2 тогда и только тогда, когда a ∈ xs и b ∈ xs.

LaTeX

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

Lean4

theorem mk_mem_sym2_iff {xs : List α} {a b : α} : s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs :=
  by
  constructor
  · intro h
    exact ⟨left_mem_of_mk_mem_sym2 h, right_mem_of_mk_mem_sym2 h⟩
  · rintro ⟨ha, hb⟩
    exact mk_mem_sym2 ha hb

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