English
Let i be a fixed index with π(i) infinite and assume every π(j) is nonempty. Then the Pi-type ∀ j, π(j) is infinite.
Русский
Пусть задан индекс i такой, что π(i) бесконечен, и для всех j множество π(j) непусто. Тогда Π j:ι π(j) бесконечно.
LaTeX
$$$\\exists i:\\iota, \\operatorname{Infinite}(\\pi i) \\land \\forall j:\\iota, \\operatorname{Nonempty}(\\pi j) \\Rightarrow \\operatorname{Infinite}(\\forall j:\\iota, \\pi j)$$$
Lean4
/-- If at least one `π i` is infinite and the rest nonempty, the pi type of all `π` is infinite. -/
theorem infinite_of_exists_right {ι : Sort*} {π : ι → Sort*} (i : ι) [Infinite <| π i] [∀ i, Nonempty <| π i] :
Infinite (∀ i : ι, π i) := by
classical
let ⟨m⟩ := @Pi.instNonempty ι π _
exact Infinite.of_injective _ (update_injective m i)
