Theorems · Definition · general topology

ContinuousMap.coeFnAlgHom

{α : Type u_1} →
  [inst : TopologicalSpace α] →
    (R : Type u_2) →
      [inst_1 : CommSemiring R] →
        {A : Type u_3} →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring A] → [inst_4 : Algebra R A] → [inst_5 : IsTopologicalSemiring A] → C(α, A) →ₐ[R] α → A

Coercion to a function as an AlgHom.

Defined in

Mathlib.Topology.ContinuousMap.Algebra

Cited by

1 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceCommSemiringTopologicalSpaceSemiringAlgebraIsTopologicalSemiring