tendsto_top

Mathlib.Order.Filter.Tendsto

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

English

For any f, Tendsto f l ⊤ holds, i.e., convergence to the top filter is always true.

Русский

Для любого отображения f предел по фильтру l к верхнему фильтру ⊤ верен всегда.

LaTeX

$$$$ \operatorname{Tendsto} f l \top $$$$

Lean4

@[simp]
theorem tendsto_top {f : α → β} {l : Filter α} : Tendsto f l ⊤ :=
  le_top

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

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

Разделы

Аффилиация

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