comp — Mathlib

English

If hv: for all a0,a1, r a0 a1 implies q (v a0) (v a1), then l.IsBoundedUnder r u implies l.IsBoundedUnder q (v ∘ u).

Русский

Если hv: для всех a0,a1, r a0 a1 имплицирует q (v a0) (v a1), то l.IsBoundedUnder r u следует l.IsBoundedUnder q (v ∘ u).

LaTeX

$$$ hv : \forall a0 a1, r a0 a1 \Rightarrow q (v a0) (v a1) \Rightarrow l.IsBoundedUnder r u \Rightarrow l.IsBoundedUnder q (v \circ u) $$$

Lean4

theorem comp {l : Filter γ} {q : β → β → Prop} {u : γ → α} {v : α → β} (hv : ∀ a₀ a₁, r a₀ a₁ → q (v a₀) (v a₁)) :
    l.IsBoundedUnder r u → l.IsBoundedUnder q (v ∘ u)
  | ⟨a, h⟩ => ⟨v a, show ∀ᶠ x in map u l, q (v x) (v a) from h.mono fun x => hv x a⟩

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