inv_cobounded — Mathlib

English

The inverse map x ↦ x⁻¹ sends cobounded to cobounded; equivalently, Tendsto Inv.inv (cobounded E) (cobounded E).

Русский

Обратная карта x⁻¹ отображает cobounded в cobounded; то есть Tendsto Inv.inv (cobounded E) (cobounded E).

LaTeX

$$Tendsto Inv.inv (cobounded E) (cobounded E)$$

Lean4

@[to_additive (attr := simp)]
theorem inv_cobounded : (cobounded E)⁻¹ = cobounded E := by
  simp only [← comap_norm_atTop', ← Filter.comap_inv, comap_comap, Function.comp_def, norm_inv']

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