mem_carrier_iff_mk_eq — Mathlib

English

An element a belongs to the carrier of a conjugacy class b if and only if ConjClasses.mk a = b.

Русский

Элемент a принадлежит носителю конъюгированного класса b тогда и только тогда, когда ConjClasses.mk a = b.

LaTeX

$$$a \in \mathrm{carrier}(b) \ \iff\ \mathrm{ConjClasses.mk}(a) = b$$$

Lean4

theorem mem_carrier_iff_mk_eq {a : α} {b : ConjClasses α} : a ∈ carrier b ↔ ConjClasses.mk a = b :=
  by
  revert b
  rw [forall_isConj]
  intro b
  rw [carrier, eq_comm, mk_eq_mk_iff_isConj, ← quotient_mk_eq_mk, Quotient.lift_mk]
  rfl

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