swap_apply_eq_iff

Mathlib.Logic.Equiv.Basic

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

English

Applying swap to z to get w is equivalent to z = swap x y applied to w.

Русский

Применение swap к z даёт w тогда и только тогда, когда z = swap x y w.

LaTeX

$$$\mathrm{swap}(x,y)(z) = w \iff z = \mathrm{swap}(x,y)(w)$$$

Lean4

theorem swap_apply_eq_iff {x y z w : α} : swap x y z = w ↔ z = swap x y w := by
  rw [apply_eq_iff_eq_symm_apply, symm_swap]

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

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

Разделы

Аффилиация

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