coprodᵢ_neBot_iff — Mathlib

English

NeBot of Coprodᵢ f is equivalent to all α i being nonempty and the existence of a NeBot component.

Русский

NeBot Coprodᵢ f эквивалентен тому, что все α i непусты и существует компонент NeBot.

LaTeX

$$NeBot (Coprodᵢ f) ↔ ∀ i, Nonempty (α i) ∧ ∃ d, NeBot (f d)$$

Lean4

@[simp]
theorem coprodᵢ_neBot_iff [∀ i, Nonempty (α i)] : NeBot (Filter.coprodᵢ f) ↔ ∃ d, NeBot (f d) := by
  simp [coprodᵢ_neBot_iff', *]

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