English
If I is inhabited and every f(i) is nonempty, and f(default) is nontrivial, then ∀ i, f(i) is nontrivial.
Русский
Если I непуст, все f(i) непусты и f(default) не тривиальна, тогда ∀ i, f(i) не тривиальны.
LaTeX
$$$[\text{Inhabited } I] \to [\forall i,\text{Nonempty}(f(i))] \to [\text{Nontrivial}(f(\text{default}))] \Rightarrow \text{Nontrivial}(\forall i, f(i))$$$
Lean4
/-- As a convenience, provide an instance automatically if `(f default)` is nontrivial.
If a different index has the non-trivial type, then use `haveI := nontrivial_at that_index`.
-/
instance nontrivial [Inhabited I] [∀ i, Nonempty (f i)] [Nontrivial (f default)] : Nontrivial (∀ i : I, f i) :=
nontrivial_at default
