English
Let ι be an infinite index type and let π : ι → Type* be a family with each π(i) nontrivial. Then the Pi-type ∀ i : ι, π(i) is infinite.
Русский
Пусть ι бесконечен и задано семейство типов π(i) над i, такое что для каждого i множество π(i) ненулево. Тогда Π i:ι π(i) бесконечно.
LaTeX
$$$\\operatorname{Infinite}(\\iota) \\land \\forall i:\\iota, \\operatorname{Nontrivial}(\\pi i) \\Rightarrow \\operatorname{Infinite}(\\forall i:\\iota, \\pi i)$$$
Lean4
instance infinite_of_left {ι : Sort*} {π : ι → Type*} [∀ i, Nontrivial <| π i] [Infinite ι] : Infinite (∀ i : ι, π i) :=
by
classical
choose m n hm using fun i => exists_pair_ne (π i)
refine Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => ?_
simp_rw [update_eq_iff, update_of_ne hne] at h
exact (hm x h.1.symm).elim
