isBoundedUnder_le_comp — Mathlib

English

For an order isomorphism e: α ≃o β, boundedness under ≤ is preserved when composing with e: IsBoundedUnder(≤) l (e ∘ u) iff IsBoundedUnder(≤) l u.

Русский

Для изоморфизма порядка e: α ≃o β сохранение ограниченности по ≤ при композиции с e: IsBoundedUnder(≤) l (e ∘ u) эквивалентно IsBoundedUnder(≤) l u.

LaTeX

$$$(IsBoundedUnder(≤)\ l\ fun x => e(u(x))) \iff IsBoundedUnder(≤)\ l\ u$$$

Lean4

@[simp]
theorem _root_.OrderIso.isBoundedUnder_le_comp [LE α] [LE β] (e : α ≃o β) {l : Filter γ} {u : γ → α} :
    (IsBoundedUnder (· ≤ ·) l fun x => e (u x)) ↔ IsBoundedUnder (· ≤ ·) l u :=
  (Function.Surjective.exists e.surjective).trans <| exists_congr fun a => by simp only [eventually_map, e.le_iff_le]

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