comap_snd_neBot_iff — Mathlib

English

There is a similar result for the second projection: comap Prod.snd f is nontrivial under nonemptiness of α.

Русский

Существует аналогичное утверждение для второй проекции: comap Prod.snd f нетривиален при непустоте α.

LaTeX

$$$\text{Nonempty } α \Rightarrow (f.comap (Prod.snd)).NeBot$$$

Lean4

@[simp]
theorem comap_snd_neBot_iff {f : Filter β} : (f.comap (Prod.snd : α × β → β)).NeBot ↔ Nonempty α ∧ f.NeBot :=
  by
  rcases isEmpty_or_nonempty α with hα | hα
  · rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]; simp
  · simp [comap_neBot_iff_frequently, hα]

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