refl — Mathlib

English

The inverse of a continuous R-algebra equivalence is again a continuous R-algebra equivalence.

Русский

Обратная к непрерывной R-алгебровой эквивалентности снова непрерывна и является R-алгебровой эквивалентностью.

LaTeX

$$$ \text{symm } e : B \to A \text{ is a ContinuousAlgEquiv }$$$

Lean4

/-- The identity isomorphism as a continuous `R`-algebra equivalence. -/
@[refl]
def refl : A ≃A[R] A where
  __ := AlgEquiv.refl
  continuous_toFun := continuous_id
  continuous_invFun := continuous_id

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