map₂_eq_bot_iff — Mathlib

English

For a binary function f: α → β → γ and a, b ∈ WithBot α, WithBot.map₂ f a b equals ⊥ if and only if a = ⊥ or b = ⊥.

Русский

Для бинарной функции f: α → β → γ и a, b ∈ WithBot α, map₂ f a b равно ⊥ тогда, когда либо a = ⊥, либо b = ⊥.

LaTeX

$$@[simp] map₂ f a b = ⊥ ⇔ a = ⊥ ∨ b = ⊥$$

Lean4

@[simp]
theorem map₂_eq_bot_iff {f : α → β → γ} {a : WithBot α} {b : WithBot β} : map₂ f a b = ⊥ ↔ a = ⊥ ∨ b = ⊥ :=
  Option.map₂_eq_none_iff

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