of_neBot_imp — Mathlib

English

If there exists a rule that from NeBot la we get Tendsto f la lb, then Tendsto f la lb holds.

Русский

Если существует правило, что для нефактора la из NeBot следует Tendsto f la lb, тогда Tendsto f la lb имеет место.

LaTeX

$$$$ (h : NeBot\ la \to Tendsto f\ la\ lb) \Rightarrow \operatorname{Tendsto} f\ la\ lb $$$$

Lean4

theorem of_neBot_imp {f : α → β} {la : Filter α} {lb : Filter β} (h : NeBot la → Tendsto f la lb) : Tendsto f la lb :=
  by
  rcases eq_or_neBot la with rfl | hla
  · exact tendsto_bot
  · exact h hla

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