instNontrivialOfNonemptyOfDefault

English

If ι is inhabited and each β i is nonempty and β default is nontrivial, then Hamming β is nontrivial.

Русский

Если множество индексов непусто, все β i непусты и β по умолчанию ненулевой, то Hamming β ненейтральна (не тривиальна).

LaTeX

$$Nontrivial(Hamming β)$$

Lean4

instance [Inhabited ι] [∀ i, Nonempty (β i)] [Nontrivial (β default)] : Nontrivial (Hamming β) :=
  Pi.nontrivial

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