mulOpposite — Mathlib

English

If α is complete then its opposite MulOpposite α is complete.

Русский

Если пространство α полно, то его противоположное пространство MulOpposite α полно.

LaTeX

$$$CompleteSpace(\\alpha) \\Rightarrow CompleteSpace(\\alpha^{op})$$$

Lean4

@[to_additive]
instance mulOpposite [CompleteSpace α] : CompleteSpace αᵐᵒᵖ where
  complete
    hf :=
    MulOpposite.op_surjective.exists.mpr <|
      let ⟨x, hx⟩ := CompleteSpace.complete (hf.map MulOpposite.uniformContinuous_unop)
      ⟨x, (map_le_iff_le_comap.mp hx).trans_eq <| MulOpposite.comap_unop_nhds _⟩

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