coprodᵢ_eq_bot_iff' — Mathlib

English

Equivalently, Coprodᵢ f = ⊥ is characterized by a condition involving emptiness and equality to bottom.

Русский

Эквивалентно Coprodᵢ f = ⊥, если выполняется условие, связанное с пустотой и равенством нулю.

LaTeX

$$Coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥$$

Lean4

theorem coprodᵢ_eq_bot_iff' : Filter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥ := by
  simpa only [not_neBot, not_and_or, funext_iff, not_forall, not_exists, not_nonempty_iff] using coprodᵢ_neBot_iff'.not

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