coprodᵢ_neBot_iff' — Mathlib

English

A NeBot condition for Coprodᵢ f can be expressed equivalently in terms of Nonempty α i and existence of a NeBot component.

Русский

НеBot условие для Coprodᵢ f эквивалентно условию о не пустых α i и существовании компонента с NeBot.

LaTeX

$$$\\mathrm{NeBot}(\\mathrm{Coprodᵢ} f) \\iff (\\forall i, \\mathrm{Nonempty}(\\alpha i)) \\land \\exists d, \\mathrm{NeBot}(f d)$$$

Lean4

theorem coprodᵢ_neBot_iff' : NeBot (Filter.coprodᵢ f) ↔ (∀ i, Nonempty (α i)) ∧ ∃ d, NeBot (f d) := by
  simp only [Filter.coprodᵢ, iSup_neBot, ← exists_and_left, ← comap_eval_neBot_iff']

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