bot_coprod — Mathlib

English

The coprod with bottom in the first coordinate reduces to comap Prod.snd of the second filter: (⊥ : Filter α).coprod l = comap Prod.snd l.

Русский

Копрод с нулём в первой координате эквивалентен упрощению через прообраз Prod.snd к второму фильтру.

LaTeX

$$$ (\\bot : Filter α).coprod l = \\operatorname{comap}(\\mathrm{Prod.snd})\\, l $$$

Lean4

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

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