tendstoUniformlyOn_iff_tendstoUniformly_comp_coe

English

Equivalent reformulation of TendstoUniformlyOn in terms of restriction to the subtype.

Русский

Эквивалентная переработка TendstoUniformlyOn через ограничение к подптипу.

LaTeX

$$$$TendstoUniformlyOn(F,f,p,s)\\iff TendstoUniformly(\\lambda i x, F(i,x)) (f \\circ (Subtype.val)) p.$$$$

Lean4

theorem tendstoUniformlyOn_iff_tendstoUniformly_comp_coe :
    TendstoUniformlyOn F f p s ↔ TendstoUniformly (fun i (x : s) => F i x) (f ∘ (↑)) p :=
  forall₂_congr fun u _ => by simp

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