other_spec' — Mathlib

English

If a ∈ z for z ∈ Sym2 α, then the pair (a, Mem.other'(h)) equals z.

Русский

Пусть a принадлежит z; тогда пара (a, другая) равна z.

LaTeX

$$$\\forall \\alpha\\; [\\mathrm{DecidableEq}(\\alpha)]\\; {a} \\;{z} \\; (h: a\\in z)\\;\\Rightarrow \\; \\mathrm{Sym2.mk}\\{ fst := a, snd := \\mathrm{Sym2.Mem.other}'(h) \\} = z$$$

Lean4

@[simp]
theorem other_spec' [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : s(a, Mem.other' h) = z :=
  by
  induction z
  aesop (add norm unfold [Sym2.rec, Quot.rec]) (rule_sets := [Sym2])

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