other_invol — Mathlib

English

If a ∈ z and Mem.other ha ∈ z, then Mem.other hb = a.

Русский

Если a ∈ z и Mem.other ha ∈ z, то Mem.other hb = a.

LaTeX

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

Lean4

theorem other_invol {a : α} {z : Sym2 α} (ha : a ∈ z) (hb : Mem.other ha ∈ z) : Mem.other hb = a := by
  classical
  rw [other_eq_other'] at hb ⊢
  convert other_invol' ha hb using 2
  apply other_eq_other'

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