mem_id

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.mem_id

English

For the identity relation on α, a1 ~[SetRel.id] a2 holds if and only if a1 = a2.

Русский

Для тождесного отношения на α равносильно a1 ~[SetRel.id] a2 тогда и только тогда, когда a1 = a2.

LaTeX

$$a_1 ~[\mathrm{SetRel.id}] a_2 \iff a_1 = a_2$$

Lean4

@[simp]
theorem mem_id : a₁ ~[SetRel.id] a₂ ↔ a₁ = a₂ :=
  .rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru