nonempty_pi_of_nonempty — Mathlib

English

If each X(i) is nonempty and ι is finite, then the product ∏ᶜ X is nonempty.

Русский

Если каждое X(i) непусто и ι конечен, то произведение ∏ᶜ X непусто.

LaTeX

$$$\\forall i, X(i) \\neq \\varnothing \\Rightarrow (\\prod^{\\mathrm{c}}_{i} X(i)) \\neq \\varnothing$$$

Lean4

instance nonempty_pi_of_nonempty {ι : Type*} [Finite ι] (X : ι → FintypeCat.{u}) [∀ i, Nonempty (X i)] :
    Nonempty (∏ᶜ X : FintypeCat.{u}) :=
  (Equiv.nonempty_congr <| productEquiv X).mpr inferInstance

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