map — Mathlib

English

If α is nonempty and f : α → β, then β is nonempty; equivalently, a witness a ∈ α yields f(a) ∈ β.

Русский

Если α непусто и есть отображение f : α → β, то β непусто; существующий элемент a ∈ α даёт элемент f(a) ∈ β.

LaTeX

$$$\operatorname{Nonempty} \alpha \to \operatorname{Nonempty} \beta$$$

Lean4

/-- Given `f : α → β`, if `α` is nonempty then `β` is also nonempty.
`Nonempty` cannot be a `functor`, because `Functor` is restricted to `Type`. -/
theorem map {α β} (f : α → β) : Nonempty α → Nonempty β
  | ⟨h⟩ => ⟨f h⟩

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