comap_eval_neBot_iff — Mathlib

English

For indexed types with all components nonempty, comap (eval i) f is nontrivial iff f is nontrivial.

Русский

Для индексированных типов, у которых все компоненты непусты, comap (eval i) f нетривиален тогда и только тогда, когда f нетривиален.

LaTeX

$$$\forall i, \operatorname{NeBot}(\operatorname{comap}(\operatorname{eval} i) f) \iff \mathrm{NeBot}(f)$$$

Lean4

@[simp]
theorem comap_eval_neBot_iff {ι : Type*} {α : ι → Type*} [∀ j, Nonempty (α j)] {i : ι} {f : Filter (α i)} :
    (comap (eval i) f).NeBot ↔ NeBot f := by simp [comap_eval_neBot_iff', *]

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