blimsup_eq_limsup_subtype — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem blimsup_eq_limsup_subtype {f : Filter β} {u : β → α} {p : β → Prop} :
    blimsup u f p = limsup (u ∘ ((↑) : {x | p x} → β)) (comap (↑) f) := by
  rw [blimsup_eq_limsup, limsup, limsup, ← map_map, map_comap_setCoe_val]

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