bliminf_eq_liminf_subtype — Mathlib

English

Let f: Filter β, u: β → α, p: β → Prop. Then bliminf u f p equals the liminf of the composed function with Subtype.val and the comap of f along the inclusion map.

Русский

Пусть f: фильтр β, u: β → α, p: β → Prop. Тогда bliminf u f p равно liminf (u ∘ Subtype.val) (comap Subtype.val f).

LaTeX

$$$ \\operatorname{bliminf} u f p = \\operatorname{liminf} (u \\circ \\operatorname{Subtype.val}) (\\operatorname{comap} \\operatorname{Subtype.val} f) $$$

Lean4

theorem bliminf_eq_liminf_subtype {f : Filter β} {u : β → α} {p : β → Prop} :
    bliminf u f p = liminf (u ∘ ((↑) : {x | p x} → β)) (comap (↑) f) :=
  blimsup_eq_limsup_subtype (α := αᵒᵈ)

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