map₂_eq_bot_iff — Mathlib

English

For f: α → β → γ, a: WithOne α, b: WithOne β, map₂ f a b = 1 iff a = 1 or b = 1.

Русский

Для f: α → β → γ, a: WithOne α, b: WithOne β, map₂ f a b = 1 тогда и только тогда, когда a = 1 или b = 1.

LaTeX

$$$\mathrm{map₂} f\ a\ b = 1 \iff a = 1 \lor b = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem map₂_eq_bot_iff {f : α → β → γ} {a : WithOne α} {b : WithOne β} : map₂ f a b = 1 ↔ a = 1 ∨ b = 1 :=
  Option.map₂_eq_none_iff

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