map2 — Mathlib

English

If Nonempty α and Nonempty β, then Nonempty γ for f : α → β → γ.

Русский

Если непусты α и β, то непусто γ для функции f : α → β → γ.

LaTeX

$$$\forall \{\alpha \beta \gamma\}, \mathrm{map}: (\alpha \to \beta \to \gamma) \to \mathrm{Nonempty}\alpha \to \mathrm{Nonempty}\beta \to \mathrm{Nonempty}\gamma$$$

Lean4

protected theorem map2 {α β γ : Sort*} (f : α → β → γ) : Nonempty α → Nonempty β → Nonempty γ
  | ⟨x⟩, ⟨y⟩ => ⟨f x y⟩

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