English
The R-subalgebra of all continuous maps α → A consists precisely of those maps whose values lie in A and are continuous, i.e., the carrier is { f: α → A | Continuous f }, forming a subalgebra of R-algebra of functions α → A.
Русский
R-подалгебра неперерывных отображений α → A состоит из всех отображений, принимающих значения в A и непрерывных, то есть носитель равен { f: α → A | Continuous f }, образуя подалгебру над R в пространстве функций α → A.
LaTeX
$$$\\text{continuousSubalgebra} : Subalgebra_R(\\alpha \\to A) \\\\ \\text{carrier} = \\{ f: \\alpha \\to A \\mid \\text{Continuous}(f) \\}. $$$
Lean4
/-- The `R`-subalgebra of continuous maps `α → A`. -/
def continuousSubalgebra : Subalgebra R (α → A) :=
{ continuousSubsemiring α A with
carrier := {f : α → A | Continuous f}
algebraMap_mem' := fun r => (continuous_const : Continuous fun _ : α => algebraMap R A r) }
