neBot — Mathlib

English

If f: α → β tends from x to y and x is a nontrivial (NeBot) filter, then y is also nontrivial.

Русский

Если f: α → β стремится от x к y и x необобщимо не-тривиален (NeBot), тогда y тоже не тривиален.

LaTeX

$$$\\forall f:\\alpha \\to \\beta, \\forall x:\\mathrm{Filter}(\\alpha), \\forall y:\\mathrm{Filter}(\\beta),\\; (\\mathrm{Tendsto} f\\ x\\ y) \\Rightarrow [x\\ \\mathrm{NeBot}] \\Rightarrow \\; y \\mathrm{NeBot}$$$

Lean4

theorem neBot {f : α → β} {x : Filter α} {y : Filter β} (h : Tendsto f x y) [hx : NeBot x] : NeBot y :=
  (hx.map _).mono h

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