instLeAtTopUnconditional

Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

URI: https://scilib.ai/kg/mathlib#SummationFilter.instLeAtTopUnconditional

English

The unconditional filter on β is LeAtTop.

Русский

Безусловный фильтр на β является верхним элементом по отношению ≤.

LaTeX

$$$\\text{LeAtTop}((\\text{unconditional }\\beta))$$$

Lean4

instance : (unconditional β).LeAtTop :=
  ⟨le_rfl⟩

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

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

Разделы

Аффилиация

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