tendsto_of_isEmpty — Mathlib

English

If α is empty, any function f: α → β and any filters la on α and lb on β satisfy Tendsto f la lb; the domain carries no obstruction to convergence.

Русский

Если A пусто, то любую функцию f: A → B и любые фильтры la на A и lb на B можно считать сопряжённой к пределу: Tendsto f la lb всегда выполняется.

LaTeX

$$$[IsEmpty\\ α] \\Rightarrow \\forall f:\\alpha \\to \\beta, \\forall la:\\mathrm{Filter}(\\alpha), \\forall lb:\\mathrm{Filter}(\\beta),\\; \\mathrm{Tendsto} f\\ la\\ lb$$$

Lean4

theorem tendsto_of_isEmpty [IsEmpty α] {f : α → β} {la : Filter α} {lb : Filter β} : Tendsto f la lb := by
  simp only [filter_eq_bot_of_isEmpty la, tendsto_bot]

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