lim — Mathlib

English

The function CU.lim is defined as the supremum of approximations: lim(c,x) = sup_n approx n c x.

Русский

Предел CU.lim задаётся как супремум аппроксимаций: lim(c,x) = sup_n approx n c x.

LaTeX

$$$\\mathrm{lim}(c,x) = \\sup_{n\\in\\mathbb{N}} \\; approx(n,c,x)$$$

Lean4

/-- A continuous function `f : X → ℝ` such that

* `0 ≤ f x ≤ 1` for all `x`;
* `f` equals zero on `c.C` and equals one outside of `c.U`;
-/
protected noncomputable def lim (c : CU P) (x : X) : ℝ :=
  ⨆ n, c.approx n x

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