other_eq_other' — Mathlib

English

For any a ∈ z, the element obtained by the 'other' operation is also in z.

Русский

Для любого a ∈ z элемент, получаемый операцией 'other', также принадлежит z.

LaTeX

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

Lean4

@[simp]
theorem other_eq_other' [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : Mem.other h = Mem.other' h := by
  rw [← congr_right, other_spec' h, other_spec]

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