setValue_right_apply_eq

Mathlib.Logic.Embedding.Basic

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

← MathLib Explorer

English

For f: α ↪ β and a,c ∈ α, (f.setValue a (f c)) c = f a.

Русский

Для f: α ↪ β и a,c ∈ α, (f.setValue a (f c)) c = f a.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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