update_eq_self_iff

Mathlib.Logic.Function.Basic

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

English

The equation update f a b = f holds if and only if b = f a.

Русский

Уравнение обновления функции равно самой функции тогда и только тогда, когда b = f a.

LaTeX

$$$update\\ f\\ a\\ b = f \\iff b = f\\ a$$$

Lean4

@[simp]
theorem update_eq_self_iff : update f a b = f ↔ b = f a := by simp [update_eq_iff]

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

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

Разделы

Аффилиация

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