isBoundedUnder_map_iff — Mathlib

English

For any φ, 𝓕, f, we have (map φ 𝓕).IsBoundedUnder r f if and only if 𝓕.IsBoundedUnder r (f ∘ φ).

Русский

Для любых отображений φ, фильтров 𝓕 и функций f верно: (map φ 𝓕).IsBoundedUnder r f эквивалентно 𝓕.IsBoundedUnder r (f ∘ φ).

LaTeX

$$$ (map \phi 𝓕).IsBoundedUnder r f \iff 𝓕.IsBoundedUnder r (f \circ \phi) $$$

Lean4

theorem isBoundedUnder_map_iff {ι κ X : Type*} {r : X → X → Prop} {f : ι → X} {φ : κ → ι} {𝓕 : Filter κ} :
    (map φ 𝓕).IsBoundedUnder r f ↔ 𝓕.IsBoundedUnder r (f ∘ φ) :=
  Iff.rfl

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