def KT (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (x : X) : C(↑(UnitalAMSpace.Maximal.Characters e), ℝ)

Equations

• KT X e x = { toFun := fun (φ : ↑(UnitalAMSpace.Maximal.Characters e)) => ↑↑φ x, continuous_toFun := ⋯ }

theorem KT_veclathom (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] : IsVecLatHom (KT X e)

theorem nonzero_KT_isometry (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (nonzero : e ≠ 0) (x : X) : UnitalAMSpace.norm e x = ‖KT X e x‖

theorem zero_KT_isometry (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (hzero : e = 0) (x : X) : UnitalAMSpace.norm e x = ‖KT X e x‖

theorem KT_unit_one (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] : KT X e e = 1

theorem KT_dense_range (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] : DenseRange (KT X e)

theorem Kakutani (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] : IsVecLatHom (KT X e) ∧ (∀ (x : X), ‖x‖ = ‖KT X e x‖) ∧ DenseRange (KT X e) ∧ KT X e e = 1