Ioc — Mathlib

English

For h₁,h₂: Tendsto u₁ lb l₁ and Tendsto u₂ lb l₁, the function x ↦ Ioc(u₁ x, u₂ x) tends to l₂.smallSets.

Русский

Пусть h₁,h₂: Tendsto u₁ lb l₁ и Tendsto u₂ lb l₁. Тогда x ↦ Ioc(u₁ x, u₂ x) стремится к l₂.smallSets.

LaTeX

$$$\\text{Tendsto } (x \\mapsto Ioc(u_1 x, u_2 x))\\ lb\\ l_2^{\\text{smallSets}}$$$

Lean4

protected theorem Ioc {l₁ l₂ : Filter α} [TendstoIxxClass Ioc l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α}
    (h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) : Tendsto (fun x => Ioc (u₁ x) (u₂ x)) lb l₂.smallSets :=
  (@TendstoIxxClass.tendsto_Ixx α Set.Ioc _ _ _).comp <| h₁.prodMk h₂

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