bind_some_right

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.bind_some_right

English

Applying bind with some on the right returns the original value: x.bind some = x.

Русский

Применение связывания с some справа возвращает исходное значение: x.bind some = x.

LaTeX

$$$ x.\bind \operatorname{Some} = x $$$

Lean4

@[simp]
theorem bind_some_right (x : Part α) : x.bind some = x :=
  by
  rw [bind_some_eq_map]
  simp [map_id']

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

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

Разделы

Аффилиация

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