English
A Pi-type ∀ i∈I, f(i) is nonempty everywhere, and if one coordinate f(i0) is nontrivial, then the entire Pi-type ∀ i, f(i) is nontrivial.
Русский
Тип Pi: если все координаты f(i) непустые и хотя бы одна f(i0) не тривиальна, то всяких функций ∀ i, f(i) не тривиален.
LaTeX
$$$\bigl(\forall i,\text{Nonempty}(f(i))\bigr) \land \text{Nontrivial}(f(i')) \Rightarrow \text{Nontrivial}(\forall i:\, I,\, f(i))$$$
Lean4
/-- A pi type is nontrivial if it's nonempty everywhere and nontrivial somewhere. -/
theorem nontrivial_at (i' : I) [inst : ∀ i, Nonempty (f i)] [Nontrivial (f i')] : Nontrivial (∀ i : I, f i) :=
by
letI := Classical.decEq (∀ i : I, f i)
exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial
