tendsto — Mathlib

English

If l has an antitone basis s, for any φ with Tendsto φ to atTop and Monotone φ, the pullback basis s ∘ φ is again an antitone basis.

Русский

Если у l есть антитональная база s, и φ удовлетворяет Tendsto φ atTop и монотонности, то s ∘ φ тоже антитональная база.

LaTeX

$$$$l.HasAntitoneBasis s \to \text{(for every monotone } \phi,\ Tendsto\phi\ atTop)\; l.HasAntitoneBasis (s \circ \phi)$$$$

Lean4

protected theorem tendsto [Preorder ι] {l : Filter α} {s : ι → Set α} (hl : l.HasAntitoneBasis s) {φ : ι → α}
    (h : ∀ i : ι, φ i ∈ s i) : Tendsto φ atTop l := fun _t ht =>
  mem_map.2 <| (hl.eventually_subset ht).mono fun i hi => hi (h i)

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