tendsto_bot

Mathlib.Order.Filter.Tendsto

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

English

For any f, Tendsto f with the bottom filter to any l is true.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem tendsto_bot {f : α → β} {l : Filter β} : Tendsto f ⊥ l := by simp [Tendsto]

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

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

Разделы

Аффилиация

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