coprod_bot — Mathlib

English

For any filter l on α and any β-type, the coproduct of l with the bottom filter on β equals the comap of the fst projection applied to l.

Русский

Для произвольного фильтра l на α и произвольного β верно, что копродукт l над β с нижним фильтром β равен прообразу по отображению fst от l.

LaTeX

$$$ l \coprod \bot = \operatorname{comap}(\mathrm{Prod.fst})\, l $$$

Lean4

@[simp]
theorem coprod_bot (l : Filter α) : l.coprod (⊥ : Filter β) = comap Prod.fst l := by simp [Filter.coprod]

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