of_eq_of

Mathlib.Computability.Reduce

URI: https://scilib.ai/kg/mathlib#ManyOneDegree.of_eq_of

English

Two encoded representatives are equal if and only if their underlying predicates are ManyOneEquiv.

Русский

Равенство кодирования p и q эквивалентно ManyOneEquiv(p,q).

LaTeX

$$$ of\\ p = of\\ q \\iff ManyOneEquiv p q $$$

Lean4

@[simp]
theorem of_eq_of {p : α → Prop} {q : β → Prop} : of p = of q ↔ ManyOneEquiv p q :=
  by
  rw [of, of, Quotient.eq'']
  simp

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

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

Разделы

Аффилиация

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