instContinuousStarMulOpposite — Mathlib

English

If R has Star, TopologicalSpace, and ContinuousStar, then ContinuousStar on the opposite type Rᵐᵒᵖ holds.

Русский

Если у R есть звезда, топологическое пространство и ContinuousStar, то ContinuousStar на противоположном типе Rᵐᵒᵖ существует.

LaTeX

$$$\mathrm{ContinuousStar}(\mathrm{MulOpposite}\, R)$$$

Lean4

instance [Star R] [TopologicalSpace R] [ContinuousStar R] : ContinuousStar Rᵐᵒᵖ :=
  ⟨MulOpposite.continuous_op.comp <| MulOpposite.continuous_unop.star⟩

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