top_mul_top

Mathlib.Order.Filter.Pointwise

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

English

Top multiplied by Top is Top: ⊤ * ⊤ = ⊤.

Русский

Умножение верхнего фильтра на верхний даёт верхний: ⊤ * ⊤ = ⊤.

LaTeX

$$$\top * \top = \top.$$$

Lean4

@[to_additive (attr := simp)]
theorem top_mul_top : (⊤ : Filter α) * ⊤ = ⊤ :=
  mul_top_of_one_le le_top

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

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

Разделы

Аффилиация

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