nontrivial_prod_right — Mathlib

English

If α is nonempty and β is nontrivial, then α × β is nontrivial.

Русский

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

LaTeX

$$$\forall {\alpha} {\beta} [\mathrm{Nonempty} \alpha] [\mathrm{Nontrivial} \beta], \mathrm{Nontrivial}(\mathrm{Prod} \; \alpha \; \beta)$$$

Lean4

instance nontrivial_prod_right [Nonempty α] [Nontrivial β] : Nontrivial (α × β) :=
  Prod.snd_surjective.nontrivial

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