coprodᵢ_neBot — Mathlib

English

There exists a canonical instance giving NeBot for coprodᵢ when all α i are nonempty.

Русский

Существует канонический экземпляр, задающий NeBot для coprodᵢ при непустых α i.

LaTeX

$$theorem coprodᵢ_neBot [∀ i, Nonempty (α i)] [Nonempty ι] (f : ∀ i, Filter (α i)) [H : ∀ i, NeBot (f i)] : NeBot (Filter.coprodᵢ f)$$

Lean4

@[instance]
theorem coprodᵢ_neBot [∀ i, Nonempty (α i)] [Nonempty ι] (f : ∀ i, Filter (α i)) [H : ∀ i, NeBot (f i)] :
    NeBot (Filter.coprodᵢ f) :=
  (H (Classical.arbitrary ι)).coprodᵢ

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