isBoundedUnder_ge_comp — Mathlib

English

For an order isomorphism e: α ≃o β, boundedness under ≥ is preserved when composing with e (plus dual form).

Русский

Для изоморфизма порядка e: α ≃o β сохранение ограниченности по ≥ при композиции с e (и двойственная форма).

LaTeX

$$$[LE \alpha] [LE \beta] (e : α \simeq o β) \Rightarrow (IsBoundedUnder(≥) l (fun x => e(u(x)))) \iff IsBoundedUnder(≥) l u$$$

Lean4

@[simp]
theorem _root_.OrderIso.isBoundedUnder_ge_comp [LE α] [LE β] (e : α ≃o β) {l : Filter γ} {u : γ → α} :
    (IsBoundedUnder (· ≥ ·) l fun x => e (u x)) ↔ IsBoundedUnder (· ≥ ·) l u :=
  OrderIso.isBoundedUnder_le_comp e.dual

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