comap_eval_neBot — Mathlib

English

There is an instance asserting NeBot of comap eval i f given nonempty α_i for all i.

Русский

Существует экземпляр, утверждающий NeBot comap (eval i) f при непустости всех α_i.

LaTeX

$$Theorem: comap_eval_neBot$$

Lean4

@[instance]
theorem comap_eval_neBot {ι : Type*} {α : ι → Type*} [∀ j, Nonempty (α j)] (i : ι) (f : Filter (α i)) [NeBot f] :
    (comap (eval i) f).NeBot :=
  comap_eval_neBot_iff.2 ‹_›

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