piFinset_const — Mathlib

English

If a finite family s of a finite type β is nonempty, then the piFinset built from a constant family is nonempty.

Русский

Если семейство s из β непусто, то piFinset, построенный из константного семейства, непуст.

LaTeX

$$$\\forall \\iota, \\text{Finite} \\Rightarrow (\\operatorname{piFinset} (\\lambda _ : \\iota, s)).\\text{Nonempty}.$$$

Lean4

theorem _root_.Finset.Nonempty.piFinset_const {ι : Type*} [Fintype ι] [DecidableEq ι] {s : Finset β} (hs : s.Nonempty) :
    (piFinset fun _ : ι ↦ s).Nonempty :=
  piFinset_nonempty.2 fun _ ↦ hs

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