bot_coprod_bot

Mathlib.Order.Filter.Prod

URI: https://scilib.ai/kg/mathlib#Filter.bot_coprod_bot

English

The coproduct of bottom filters on α and β is the bottom filter on α×β.

Русский

Копродукт нулевых фильтров на α и β равен нулевому фильтру на α×β.

LaTeX

$$$(\bot : \text{Filter } \alpha) \coprod (\bot : \text{Filter } \beta) = (\bot : \text{Filter } (\alpha \times \beta))$$$

Lean4

theorem bot_coprod_bot : (⊥ : Filter α).coprod (⊥ : Filter β) = ⊥ := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru