update_ne_self_iff

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.update_ne_self_iff

English

The statement update f a b ≠ f is equivalent to b ≠ f a.

Русский

Утверждение обновления отличного от исходной функции эквивалентно $b \neq f(a)$.

LaTeX

$$$\\mathrm{update}\\ f\\ a\\ b \\neq f \\iff b \\neq f\\ a$$$

Lean4

theorem update_ne_self_iff : update f a b ≠ f ↔ b ≠ f a :=
  update_eq_self_iff.not

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

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

Разделы

Аффилиация

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