div_div

Mathlib.Order.Filter.Pointwise

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

← MathLib Explorer

English

If hf: Tendsto m f1 f2 and hg: Tendsto m g1 g2, then Tendsto m (f1 / g1) (f2 / g2).

Русский

Если hf: Tendsto m f1 f2 и hg: Tendsto m g1 g2, то Tendsto m (f1 / g1) (f2 / g2).

LaTeX

$$Tendsto m f1 f2 → Tendsto m g1 g2 → Tendsto m (f1 / g1) (f2 / g2)$$

Lean4

@[to_additive]
protected theorem div_div (hf : Tendsto m f₁ f₂) (hg : Tendsto m g₁ g₂) : Tendsto m (f₁ / g₁) (f₂ / g₂) :=
  (Filter.map_div m).trans_le <| Filter.div_le_div hf hg

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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