Theorems · Theorem · functional analysis

NonUnitalSubalgebra.topologicalClosure_map_le

∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : TopologicalSpace A]
  [inst_2 : NonUnitalSemiring A] [inst_3 : Module R A] [inst_4 : ContinuousConstSMul R A]
  [inst_5 : IsSemitopologicalSemiring A] [inst_6 : TopologicalSpace B] [inst_7 : NonUnitalSemiring B]
  [inst_8 : Module R B] [inst_9 : IsTopologicalSemiring B] [inst_10 : ContinuousConstSMul R B]
  (s : NonUnitalSubalgebra R A) {φ : A →ₙₐ[R] B},
  IsClosedMap ⇑φ → (NonUnitalSubalgebra.map φ s).topologicalClosure ≤ NonUnitalSubalgebra.map φ s.topologicalClosure

Defined in

Mathlib.Topology.Algebra.NonUnitalAlgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringTopologicalSpaceNonUnitalSemiringModuleContinuousConstSMulIsSemitopologicalSemiringTopologicalSpaceNonUnitalSemiringModuleIsTopologicalSemiringContinuousConstSMul