setValue_eq

Mathlib.Logic.Embedding.Basic

URI: https://scilib.ai/kg/mathlib#Function.Embedding.setValue_eq

← MathLib Explorer

English

For f: α ↪ β and a,b, the updated embedding f.setValue a b satisfies (f.setValue a b) a = b.

Русский

Для вложения f: α ↪ β и элементов a,b выполняется (f.setValue a b) a = b.

LaTeX

$$$(f.setValue\\ a\\ b)\\ a = b$$$

Lean4

@[simp]
theorem setValue_eq {α β} (f : α ↪ β) (a : α) (b : β) [∀ a', Decidable (a' = a)] [∀ a', Decidable (f a' = b)] :
    setValue f a b a = b := by simp [setValue]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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