bot_mul

Mathlib.Order.Filter.Pointwise

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

English

⊥ * g = ⊥; multiplying by the bottom filter on the left yields the bottom filter.

Русский

⊥ * g = ⊥; левая умножение на нижний фильтр даёт нижний фильтр.

LaTeX

$$$$ \bot * g = \bot. $$$$

Lean4

@[to_additive (attr := simp)]
theorem bot_mul : ⊥ * g = ⊥ :=
  map₂_bot_left

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

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

Разделы

Аффилиация

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