map₂_eq_none_iff

Mathlib.Data.Option.NAry

URI: https://scilib.ai/kg/mathlib#Option.map₂_eq_none_iff

English

map₂ f a b equals none if and only if a is none or b is none.

Русский

map₂ f a b равно none тогда, когда a равно none или b равно none.

LaTeX

$$$ map_2 f\ a\ b = \mathrm{none} \iff a = \mathrm{none} \lor b = \mathrm{none} $$$

Lean4

@[simp]
theorem map₂_eq_none_iff : map₂ f a b = none ↔ a = none ∨ b = none := by grind

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

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

Разделы

Аффилиация

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