comap_fst_neBot_iff — Mathlib

English

There is an instance giving NeBot for f comapped via Prod.fst when β is nonempty.

Русский

Существует экземпляр, дающий NeBot для f, сопряженного с Prod.fst, когда β не пусто.

LaTeX

$$[Nonempty β] {f} [NeBot f] : (f.comap (Prod.fst)).NeBot$$

Lean4

@[simp]
theorem comap_fst_neBot_iff {f : Filter α} : (f.comap (Prod.fst : α × β → α)).NeBot ↔ f.NeBot ∧ Nonempty β :=
  by
  cases isEmpty_or_nonempty β
  · rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]; simp [*]
  · simp [comap_neBot_iff_frequently, *]

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