tendsto_atBot_pure

Mathlib.Order.Filter.AtTopBot.Tendsto

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

English

Dual statement: Tendsto f atBot to the pure image of f(⊥).

Русский

Двойственное утверждение: Tendsto f atBot переходит в чистый образ f(⊥).

LaTeX

$$$$ \operatorname{Tendsto} f\ atBot \to \text{pure}(f\bot). $$$$

Lean4

theorem tendsto_atBot_pure [PartialOrder α] [OrderBot α] (f : α → β) : Tendsto f atBot (pure <| f ⊥) :=
  @tendsto_atTop_pure αᵒᵈ _ _ _ _

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

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

Разделы

Аффилиация

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