symm_apply_eq

Mathlib.Order.RelIso.Basic

URI: https://scilib.ai/kg/mathlib#RelIso.symm_apply_eq

English

For e : r ≃r s, e.symm x = y iff x = e y.

Русский

Для e : r ≃r s, e.symm x = y ⇔ x = e y.

LaTeX

$$$$ e.symm x = y \\iff x = e y. $$$$

Lean4

theorem symm_apply_eq (e : r ≃r s) {x y} : e.symm x = y ↔ x = e y :=
  e.toEquiv.symm_apply_eq

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

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

Разделы

Аффилиация

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