comap_norm_atTop' — Mathlib

English

The cobounded filter on E is generated by the preimages of norm-bounded sets; in particular, cobounded is generated by norm preimages of sets of the form {x : ∥x∥ ≤ r}.

Русский

Обозначение cobounded генерируется посредством предобразов нормированных шаров: cobounded = HasBasis p s с p ≡ True и s(i) = {x : ∥x∥ ≤ r}.

LaTeX

$$$HasBasis (cobounded E) (fun _ => True) \\{x\\| \\|x\\| ≤ r\\}$$$

Lean4

@[to_additive (attr := simp) comap_norm_atTop]
theorem comap_norm_atTop' : comap norm atTop = cobounded E := by
  simpa only [dist_one_right] using comap_dist_right_atTop (1 : E)

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