nontrivial — Mathlib

English

If α is nonempty and β is nontrivial, then the function space α → β is nontrivial.

Русский

Если α непуст, а β не тривиальна, то множество функций α → β не тривиально.

LaTeX

$$$[\text{Nonempty}(\alpha)] \land [\text{Nontrivial}(\beta)] \Rightarrow \text{Nontrivial}(\alpha \to \beta)$$$

Lean4

instance nontrivial [h : Nonempty α] [Nontrivial β] : Nontrivial (α → β) :=
  h.elim fun a ↦ Pi.nontrivial_at a

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