apply_eq_iff_eq_symm_apply

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.apply_eq_iff_eq_symm_apply

English

For any e: α ≃ β, y = e.symm x ↔ e y = x; equivalence between equality under symm and image equality.

Русский

Для любого e: α ≃ β, y = e.symm x ⇔ e y = x; равносильность между равенством после симм и отображением.

LaTeX

$$$y = e^{-1} x \\iff e(y)=x$$$

Lean4

theorem apply_eq_iff_eq_symm_apply {x : α} {y : β} (f : α ≃ β) : f x = y ↔ x = f.symm y := by grind

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

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

Разделы

Аффилиация

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