map₂_bot_right

Mathlib.Order.Filter.NAry

URI: https://scilib.ai/kg/mathlib#Filter.map₂_bot_right

English

Similarly, map₂ m f ⊥ equals ⊥.

Русский

Аналогично, map₂ m f ⊥ равно ⊥.

LaTeX

$$$ map_2 m f \bot = \bot $$$

Lean4

@[simp]
theorem map₂_bot_right : map₂ m f ⊥ = ⊥ :=
  map₂_eq_bot_iff.2 <| .inr rfl

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

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

Разделы

Аффилиация

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