apply_bliminf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.OrderIso.apply_bliminf [CompleteLattice γ] (e : α ≃o γ) : e (bliminf u f p) = bliminf (e ∘ u) f p :=
  e.dual.apply_blimsup

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