English
A variant of comap_eval_neBot' for indexed families shows equivalence with a product of nonempty indices.
Русский
Вариант comap_eval_neBot' для индексированных семейств показывает эквивалентность с произведением не пустых индексов.
LaTeX
$$$\text{NeBot}(\operatorname{comap} \operatorname{eval} f) \iff (\forall i, \Nonempty(\alpha_i)) \land \mathrm{NeBot}(f)$$$
Lean4
theorem comap_eval_neBot_iff' {ι : Type*} {α : ι → Type*} {i : ι} {f : Filter (α i)} :
(comap (eval i) f).NeBot ↔ (∀ j, Nonempty (α j)) ∧ NeBot f :=
by
rcases isEmpty_or_nonempty (∀ j, α j) with H | H
· rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]
simp [← Classical.nonempty_pi]
· have : ∀ j, Nonempty (α j) := Classical.nonempty_pi.1 H
simp [comap_neBot_iff_frequently, *]
