nontrivial_prod_left — Mathlib

English

If a type α is nontrivial and a type β is nonempty, then the Cartesian product α × β is nontrivial.

Русский

Если тип α не тривиален и тип β непуст, то произведение α × β не тривиально.

LaTeX

$$$\text{Nontrivial}(\alpha) \land \text{Nonempty}(\beta) \Rightarrow \text{Nontrivial}(\alpha \times \beta)$$$

Lean4

instance nontrivial_prod_left [Nontrivial α] [Nonempty β] : Nontrivial (α × β) :=
  Prod.fst_surjective.nontrivial

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