apply_blimsup_le — Mathlib

English

Let g be a suitable sSupHom. Then g(blimsup u f p) ≤ blimsup (g ∘ u) f p.

Русский

Пусть g — отображение типа sSupHom. Тогда g(blimsup u f p) ≤ blimsup(g ∘ u) f p.

LaTeX

$$$g(\\operatorname{blimsup} u f p) \\le \\operatorname{blimsup}(g \\circ u) f p$$$

Lean4

theorem _root_.sSupHom.apply_blimsup_le [CompleteLattice γ] (g : sSupHom α γ) :
    g (blimsup u f p) ≤ blimsup (g ∘ u) f p :=
  by
  simp only [blimsup_eq_iInf_biSup, Function.comp]
  refine ((OrderHomClass.mono g).map_iInf₂_le _).trans ?_
  simp only [_root_.map_iSup, le_refl]

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