apply_blimsup — Mathlib

English

If e is an order isomorphism between α and γ, then applying e to blimsup(u,f,p) yields blimsup(e ∘ u, f, p).

Русский

Если e — перестановка по порядку между α и γ, то применение e к blimsup(u,f,p) даёт blimsup( e ∘ u , f, p ).

LaTeX

$$$e\\,(\\operatorname{blimsup}u f p) = \\operatorname{blimsup}(e \\circ u) f p$$$

Lean4

theorem _root_.OrderIso.apply_blimsup [CompleteLattice γ] (e : α ≃o γ) : e (blimsup u f p) = blimsup (e ∘ u) f p := by
  simp only [blimsup_eq, map_sInf, Function.comp_apply, e.image_eq_preimage, Set.preimage_setOf_eq, e.le_symm_apply]

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