Tendsto — Mathlib

English

Coercion preserves Tendsto: f tends to lb iff its germ represents Tendsto.

Русский

Вмещение сохраняет предел: f сходится к lb тогда и только тогда, когда его зародыш содержит предел.

LaTeX

$$$ (f : \mathrm{Germ}(l, \beta)).\text{Tendsto} lb \iff \mathrm{Tendsto}(f) l lb $$$

Lean4

/-- A germ at `l` of maps from `α` to `β` tends to `lb : Filter β` if it is represented by a map
which tends to `lb` along `l`. -/
protected def Tendsto (f : Germ l β) (lb : Filter β) : Prop :=
  liftOn f (fun f => Tendsto f l lb) fun _f _g H => propext (tendsto_congr' H)

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