comp_strictMono — Mathlib

English

If l HasAntitoneBasis s and φ is StrictMono, then l HasAntitoneBasis (s ∘ φ).

Русский

Если у фильтра l есть антитональная база s и φ строго монотонна, то l HasAntitoneBasis (s ∘ φ).

LaTeX

$$$$l.HasAntitoneBasis (s \circ φ)$$$$

Lean4

theorem comp_strictMono {l : Filter α} {s : ℕ → Set α} (hs : l.HasAntitoneBasis s) {φ : ℕ → ℕ} (hφ : StrictMono φ) :
    l.HasAntitoneBasis (s ∘ φ) :=
  hs.comp_mono hφ.monotone hφ.tendsto_atTop

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