isBoundedUnder_ge_comp — Mathlib

English

If v is antitone and l is bounded above by u with respect to ≤, then l is bounded above by v ∘ u with respect to ≥.

Русский

Если v антитонна и l ограничен сверху по ≤ через u, то l ограничен сверху по ≥ через v∘u.

LaTeX

$$[Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Antitone v) (hl : l.IsBoundedUnder (\le) u) : l.IsBoundedUnder (\ge) (v ∘ u)$$

Lean4

theorem _root_.Antitone.isBoundedUnder_ge_comp [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β}
    (hv : Antitone v) (hl : l.IsBoundedUnder (· ≤ ·) u) : l.IsBoundedUnder (· ≥ ·) (v ∘ u) :=
  hl.comp hv

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