Theorems · Theorem · functional analysis

NormedSpace.exp_mem

∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] {R : Type u_3}
  {S : Type u_4} [inst_3 : Monoid R] [inst_4 : SMul ℚ R] [inst_5 : MulAction R 𝔸] [inst_6 : Algebra ℚ 𝔸]
  [IsScalarTower ℚ R 𝔸] [inst_8 : SetLike S 𝔸] [SubsemiringClass S 𝔸] [SMulMemClass S R 𝔸] {s : S},
  IsClosed ↑s → ∀ {x : 𝔸}, x ∈ s → NormedSpace.exp x ∈ s

A subalgebra of 𝔸 that is closed topologically and under ℚ-scaling is closed under exp.

Defined in

Mathlib.Analysis.Normed.Algebra.Exponential

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingTopologicalSpaceIsTopologicalRingMonoidSMulMulActionAlgebraIsScalarTowerSetLikeSubsemiringClassSMulMemClass