other_invol' — Mathlib

English

If a ∈ z and Mem.other'(ha) ∈ z, then Mem.other'(Mem.other'(ha)) = a.

Русский

Если a ∈ z и Mem.other'(ha) ∈ z, то Mem.other'(Mem.other'(ha)) = a.

LaTeX

$$$\\forall \\alpha\\; [\\mathrm{DecidableEq}(\\alpha)]\\; (ha: a\\in z)\\; (hb: \\mathrm{Mem.other}'ha \\in z)\\;\\Rightarrow \\mathrm{Mem.other}'hb = a$$$

Lean4

theorem other_invol' [DecidableEq α] {a : α} {z : Sym2 α} (ha : a ∈ z) (hb : Mem.other' ha ∈ z) : Mem.other' hb = a :=
  by
  induction z
  aesop (rule_sets := [Sym2]) (add norm unfold [Sym2.rec, Quot.rec])

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