fun_eq_comp

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.fun_eq_comp

English

The relation (f · = ·) ∘r r equals (r · f).

Русский

Отношение (f · = ·) ∘r r равно (r · f).

LaTeX

$$$\forall f:\gamma\to\alpha,\; (f\cdot = \cdot) \circ_r r = (r \lvert f\cdot)$$$

Lean4

@[simp]
theorem fun_eq_comp (f : γ → α) : (f · = ·) ∘r r = (r <| f ·) :=
  by
  ext x y
  simp [Comp]

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

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

Разделы

Аффилиация

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