other_mem' — Mathlib

English

Same as Mem.other', asserting the element produced by 'other'' lies in z.

Русский

Та же самая формула для элемента, полученного через 'other''.

LaTeX

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

Lean4

theorem other_mem' [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : Mem.other' h ∈ z :=
  by
  rw [← other_eq_other']
  exact other_mem h

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