map₂_eq_top_iff — Mathlib

English

For a binary map, map₂ f a b equals top exactly when at least one argument is top.

Русский

Для двоичного отображения map₂ f a b равно топу тогда, когда хотя бы один аргумент равен топу.

LaTeX

$$$\\mathrm{WithTop.map₂}\\ f\\ a\\ b = \\top \\iff a = \\top \\lor b = \\top$$$

Lean4

@[simp]
theorem map₂_eq_top_iff {f : α → β → γ} {a : WithTop α} {b : WithTop β} : map₂ f a b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
  Option.map₂_eq_none_iff

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