finset_inf_nhds — Mathlib

English

Let s be a finite set. The infimum operation over s preserves Tendsto under suitable conditions, mirroring the supremum case in dual form.

Русский

Для конечного множества s сохранение сходимости инфимумом аналогично случаю с верхней гранью в двойственном виде.

LaTeX

$$$\\text{Finset Inf Tendsto}$$$

Lean4

theorem finset_inf_nhds [SemilatticeInf L] [OrderTop L] [ContinuousInf L] (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :
    Tendsto (s.inf f) l (𝓝 (s.inf g)) :=
  finset_sup_nhds (L := Lᵒᵈ) hs

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