isBoundedUnder — Mathlib

English

If u preserves r in the sense that r a0 a1 implies q(u a0) (u a1) for all a0, a1, and f is r-bounded, then f is q-bounded under u.

Русский

Если функция u сохраняет отношение r в смысле, что r a0 a1 имплицирует q(u a0) (u a1) для любых a0, a1, и фильтр f ограничен по r, то f ограничен по q через u.

LaTeX

$$$ hu : \forall a0 a1,\ r\ a0 a1 \Rightarrow q (u a0) (u a1) \Rightarrow f.IsBounded r \Rightarrow f.IsBoundedUnder q u $$$

Lean4

theorem isBoundedUnder {q : β → β → Prop} {u : α → β} (hu : ∀ a₀ a₁, r a₀ a₁ → q (u a₀) (u a₁)) :
    f.IsBounded r → f.IsBoundedUnder q u
  | ⟨b, h⟩ => ⟨u b, show ∀ᶠ x in f, q (u x) (u b) from h.mono fun x => hu x b⟩

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