instNonempty — Mathlib

English

If each M(a) is nonempty, then the ultraproduct (u).Product M is nonempty.

Русский

Если каждый M(a) непуст, то ультропроизведение (u).Product M непусто.

LaTeX

$$$\forall a:α, M(a) \neq \emptyset \Rightarrow (u:\text{Filter } α).Product M \neq \emptyset$$$

Lean4

nonrec instance instNonempty : Nonempty ((u : Filter α).Product M) :=
  letI : ∀ a, Inhabited (M a) := fun _ => Classical.inhabited_of_nonempty'
  inferInstance

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