inv_inv

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.Tendsto.inv_inv

English

If Tendsto m f1 f2, then Tendsto m f1^{-1} f2^{-1}.

Русский

Если Tendsto m f1 f2, то Tendsto m f1^{-1} f2^{-1}.

LaTeX

$$Tendsto m f1 f2 → Tendsto m f1^{-1} f2^{-1}$$

Lean4

@[to_additive]
protected theorem inv_inv : Tendsto m f₁ f₂ → Tendsto m f₁⁻¹ f₂⁻¹ := fun hf =>
  (Filter.map_inv' m).trans_le <| Filter.inv_le_inv hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru