map_id

Mathlib.Probability.ProbabilityMassFunction.Constructions

URI: https://scilib.ai/kg/mathlib#PMF.map_id

English

Mapping with the identity does nothing: map id p = p.

Русский

Отображение по тождественному отображению не меняет PMF: map id p = p.

LaTeX

$$$\\text{map id } p = p$$$

Lean4

theorem map_id : map id p = p :=
  bind_pure _

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

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

Разделы

Аффилиация

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