compactSpace_optimalGHCoupling — Mathlib

English

The optimal coupling space for two compact spaces is itself compact.

Русский

Оптимальное связывание двух компактных пространств обладает компактостью.

LaTeX

$$CompactSpace (OptimalGHCoupling X Y)$$

Lean4

/-- The optimal coupling between two compact spaces `X` and `Y` is still a compact space -/
instance compactSpace_optimalGHCoupling : CompactSpace (OptimalGHCoupling X Y) :=
  ⟨by
    rw [← range_quotient_mk']
    exact
      isCompact_range
        (continuous_sum_dom.2 ⟨(isometry_optimalGHInjl X Y).continuous, (isometry_optimalGHInjr X Y).continuous⟩)⟩

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