tendstoLocallyUniformlyOn_univ — Mathlib

English

Equivalence: TendstoLocallyUniformlyOn F f p univ is equivalent to TendstoLocallyUniformly F f p.

Русский

Эквивалентность: TendstoLocallyUniformlyOn F f p univ эквивалентно TendstoLocallyUniformly F f p.

LaTeX

$$$\\text{TendstoLocallyUniformlyOn } F\\ f\\ p\\ \\text{ univ } \\iff \\text{ TendstoLocallyUniformly } F\\ f\\ p$$$

Lean4

theorem tendstoLocallyUniformlyOn_univ : TendstoLocallyUniformlyOn F f p univ ↔ TendstoLocallyUniformly F f p := by
  simp [TendstoLocallyUniformlyOn, TendstoLocallyUniformly, nhdsWithin_univ]

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