instCocompactMapClass — Mathlib

English

The composition of cocompact continuous maps is again a cocompact map: if f ∈ CocompactMap β γ and g ∈ CocompactMap α β, then f ∘ g ∈ CocompactMap α γ.

Русский

Произведение кококомпактных отображений даёт новое коккомпактное отображение: если f ∈ CocompactMap β γ и g ∈ CocompactMap α β, то f ∘ g ∈ CocompactMap α γ.

LaTeX

$$$\\text{def } comp(f,g) := \\langle f \\circ g, \\text{cocompact_tendsto}(f) \\circ \\text{cocompact_tendsto}(g) \\rangle$$$

Lean4

instance : CocompactMapClass (CocompactMap α β) α β
    where
  map_continuous f := f.continuous_toFun
  cocompact_tendsto f := f.cocompact_tendsto'

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