The mathematical goal
A single unital, simple, infinite-dimensional C*-algebra has one unitary-equivalence class of nonzero irreducible representations and a faithful tracial representation on a separable Hilbert space. The normalized trace of its CAR subalgebra extends uniquely among all states of the same generated algebra.
Exact source: MathlibAnnex v0.4.0 Project entry · Source manifest
Declaration Cards are in preparation. These 466 tiles describe exact declarations and their Project graph; no canonical Card links are active.
Scope
The principal construction concerns complex C*-algebras and nonzero irreducible representations. Its fixed algebra and separable faithful tracial representation require no CH hypothesis. CH enters only in the statement equating the continuum with aleph one and the corresponding density-character existence result. The general reverse density obstruction also allows nonunital algebras.
Scope limits
No canonical Declaration Cards are active in this Companion. Source qualification, source-exposition correspondence and human mathematical review are separate records; no line-by-line independent human proof audit is claimed. The CH biconditional is not a forcing or metatheoretic independence certificate. Corollary 6.2 of Brief Draft R1 is mapped to exact formal endpoints together with a standard Hilbert-space consequence. The orthonormal-basis cardinality statement is the standard consequence, not a direct Lean endpoint supplied in this release; it is not a Hamel-dimension statement.
Proof architecture
CAR source, pure states and decreasing flags
The CAR source supplies the pure-state compression and decreasing flags used to distinguish the selected irreducible models. The normalized trace controls the same flags in the later tracial argument.
Shell matching and the generated algebra
Matched shells and their strong operator sums define the concrete generators. The construction keeps one fixed generated C*-algebra rather than replacing it by another algebra with similar relations.
AtomicCounterexampleAlgebra · atomicCounterexampleRepresentation
Capture and classification of irreducible representations
The capture argument compares nonzero irreducible representations of the generated algebra with its fixed irreducible model. The resulting endpoint gives the single equivalence class and the ordinary counterexample properties.
State extension and the tracial GNS space
Extend the CAR trace to a state of the same algebra. The CAR-cyclic subspace reduces the target generators and equals the full cyclic GNS space. The extension is then identified uniquely, and the tracial and faithful properties are obtained on this same model.
cyclicSubspace_eq_top_of_trace_of_cyclic · existsUnique_tracial_state · eq_traceExtension_of_mem_stateSpace_of_mul_comm · existsUnique_state_extension_trace
Faithful separable representation without separable irreducibles
The trace GNS construction gives a faithful representation on a separable Hilbert space. This representation is reducible; the exclusion theorem applies to every nonzero irreducible representation on a separable Hilbert space, not merely to the representation selected here.
Density, cardinality and CH
Faithful separable representability bounds the cardinality of the fixed algebra by the continuum. The general lower bound for dense subsets of ordinary Naimark counterexamples yields equality of its cardinality and norm density with the continuum. Combining the example with the general obstruction gives the CH biconditional for density aleph one.
cardinalMk_atomicCounterexampleAlgebra · hasDensityCharacter_atomicCounterexampleAlgebra · continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity
Boundary Inputs
4939 exact Boundary Inputs: EXTERNAL_COMPILED_DECLARATION 3571, OMITTED_INTERNAL_NATIVE_DECLARATION 1368. Selected reachability is retained through every omitted internal declaration.
Inspect Boundary Inputs
OfNat.ofNat— Compiled external provider used by selected Project declarations.Complex— Compiled external provider used by selected Project declarations.Eq— Compiled external provider used by selected Project declarations.DFunLike.coe— Compiled external provider used by selected Project declarations.Complex.instSemiring— Compiled external provider used by selected Project declarations.Semiring.toNonAssocSemiring— Compiled external provider used by selected Project declarations.Zero.toOfNat0— Compiled external provider used by selected Project declarations.AddCommMonoid.toAddMonoid— Compiled external provider used by selected Project declarations.AddMonoid.toAddZeroClass— Compiled external provider used by selected Project declarations.AddZeroClass.toAddZero— Compiled external provider used by selected Project declarations.Complex.instNonUnitalCommRing— Compiled external provider used by selected Project declarations.NonUnitalCommRing.toNonUnitalNonAssocCommRing— Compiled external provider used by selected Project declarations.NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing— Compiled external provider used by selected Project declarations.congrArg— Compiled external provider used by selected Project declarations.AddZero.toZero— Compiled external provider used by selected Project declarations.
Dependency-first reading route
Levels belong to this Project. Select a level or follow a relation to another declaration tile.
Level 0
8 declarationsconcreteTarget
MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
None in this Project
Used by in this Project
ambientInclusion, instIsClosed, generatorShow 2 more
RepresentativeShellFamily
MathlibAnnex.CStarAlgebra.CAR.RepresentativeShellFamily
Exact source-authored inductive in the Naimark construction.
Immediate prerequisites in this Project
None in this Project
Used by in this Project
ShellFamilyEndpoint, homogeneityShellFamily, representativeShellDataShow 1 more
Stage
MathlibAnnex.CStarAlgebra.CAR.Stage
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
None in this Project
Used by in this Project
amplify, finrank_stage, matrixUnit
stepIndexEquiv
MathlibAnnex.CStarAlgebra.CAR.stepIndexEquiv
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
None in this Project
Used by in this Project
step
transportBudget
MathlibAnnex.CStarAlgebra.CAR.transportBudget
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
None in this Project
Used by in this Project
summable_transportBudget, tendsto_transportBudget_zero, transportBudget_pos
IsSimpleCStarAlgebra
MathlibAnnex.CStarAlgebra.IsSimpleCStarAlgebra
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
None in this Project
Used by in this Project
isSimpleCStarAlgebra_limit, isSimpleCStarAlgebra_shellFamilyTarget
exists_shell_of_approximately_inner
MathlibAnnex.CStarAlgebra.exists_shell_of_approximately_inner
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
None in this Project
Used by in this Project
exists_shell_family_of_approximately_inner
stateSpace
MathlibAnnex.CStarAlgebra.stateSpace
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
None in this Project
Used by in this Project
eq_rootFunctional_of_apply_rootProjection_eq_one, restrictState_mem_stateSpace, rootFunctional_mem_stateSpace
Level 1
20 declarationsambientInclusion
MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
concreteTarget
Used by in this Project
ambientInclusion_injective, exists_irreducible_atomicShellModel, intertwines_concreteTarget_of_generators
instIsClosed
MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget.instIsClosed
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
concreteTarget
Used by in this Project
eq_top_of_source_mem_of_generator_mem, exists_irreducible_atomicShellModel, intertwines_concreteTarget_of_generatorsShow 1 more
generator
MathlibAnnex.CStarAlgebra.AtomicConstruction.generator
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
concreteTarget
Used by in this Project
eq_top_of_source_mem_of_generator_mem, generator_coe, intertwines_concreteTarget_of_generators
sourceHom
MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
concreteTarget
Used by in this Project
eq_top_of_source_mem_of_generator_mem, intertwines_concreteTarget_of_generators, reduces_concreteTarget_of_generatorsShow 3 more
ShellFamilyEndpoint
MathlibAnnex.CStarAlgebra.CAR.ShellFamilyEndpoint
Exact source-authored inductive in the Naimark construction.
Immediate prerequisites in this Project
RepresentativeShellFamily
Used by in this Project
AtomicCounterexampleEndpoint, shellFamilyEndpoint
amplify
MathlibAnnex.CStarAlgebra.CAR.amplify
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
Stage
Used by in this Project
amplify_injective, step
finrank_stage
MathlibAnnex.CStarAlgebra.CAR.finrank_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
Stage
Used by in this Project
not_finiteDimensional
matrixUnit
MathlibAnnex.CStarAlgebra.CAR.matrixUnit
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
Stage
Used by in this Project
limitMatrixUnit, matrixUnit_apply, matrixUnit_mul_of_ne
rootLinear
MathlibAnnex.CStarAlgebra.CAR.rootLinear
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
Stage
Used by in this Project
rootFunctional, rootLinear_nonneg
rootProjection
MathlibAnnex.CStarAlgebra.CAR.rootProjection
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
Stage
Used by in this Project
rootFlag, rootProjection_mul_mul, stageTrace_rootProjection
stageFiniteDimensional
MathlibAnnex.CStarAlgebra.CAR.stageFiniteDimensional
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
Stage
Used by in this Project
stageSeparableSpace
stageIsSimpleRing
MathlibAnnex.CStarAlgebra.CAR.stageIsSimpleRing
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
Stage
Used by in this Project
rootRepresentation_stage_injective
stageNontrivial
MathlibAnnex.CStarAlgebra.CAR.stageNontrivial
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
Stage
Used by in this Project
preNontrivial
stageTraceLinear
MathlibAnnex.CStarAlgebra.CAR.stageTraceLinear
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
Stage
Used by in this Project
norm_stageTraceLinear_le
summable_transportBudget
MathlibAnnex.CStarAlgebra.CAR.summable_transportBudget
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
transportBudget
Used by in this Project
leftAutomorphisms_cauchy, leftAutomorphisms_symm_cauchy, rightAutomorphisms_cauchyShow 1 more
tendsto_transportBudget_zero
MathlibAnnex.CStarAlgebra.CAR.tendsto_transportBudget_zero
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
transportBudget
Used by in this Project
tendsto_outputAutomorphisms_state
transportBudget_pos
MathlibAnnex.CStarAlgebra.CAR.transportBudget_pos
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
transportBudget
Used by in this Project
nonempty_initialState, nonempty_transition
IsPureState
MathlibAnnex.CStarAlgebra.IsPureState
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
stateSpace
Used by in this Project
PureStateHomogeneity, RepresentativeShellData, hasInnerIntertwiningSequence_of_pureShow 2 more
exists_shell_family_of_approximately_inner
MathlibAnnex.CStarAlgebra.exists_shell_family_of_approximately_inner
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_shell_of_approximately_inner
Used by in this Project
representativeShellDataOfHomogeneity
positiveLinearMapOfMemStateSpace
MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
stateSpace
Used by in this Project
exists_nonzero_targetFixedSpace, traceExtensionPositive, positiveLinearMapOfMemStateSpace_one
Level 2
22 declarationsambientInclusion_injective
MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ambientInclusion
Used by in this Project
shellFamilyInclusion_injective
eq_top_of_source_mem_of_generator_mem
MathlibAnnex.CStarAlgebra.AtomicConstruction.eq_top_of_source_mem_of_generator_mem
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
instIsClosed, generator, sourceHom
Used by in this Project
starAlgHom_ext
generator_coe
MathlibAnnex.CStarAlgebra.AtomicConstruction.generator_coe
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
generator
Used by in this Project
exists_irreducible_atomicShellModel
intertwines_concreteTarget_of_generators
MathlibAnnex.CStarAlgebra.AtomicConstruction.intertwines_concreteTarget_of_generators
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ambientInclusion, instIsClosed, generatorShow 1 more
Used by in this Project
ambientInclusion_unitaryEquivalent
reduces_concreteTarget_of_generators
MathlibAnnex.CStarAlgebra.AtomicConstruction.reduces_concreteTarget_of_generators
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
instIsClosed, generator, sourceHom
Used by in this Project
isIrreducible_restrictedRepresentation_of_all_fixed_bot, reduces_cyclicSubspace_of_trace
sourceHom_coe
MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom_coe
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
sourceHom
Used by in this Project
exists_irreducible_atomicShellModel
sourceHom_injective
MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
sourceHom
Used by in this Project
exists_completedAtomicShellModel
amplify_injective
MathlibAnnex.CStarAlgebra.CAR.amplify_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
amplify
Used by in this Project
step_injective
matrixUnit_apply
MathlibAnnex.CStarAlgebra.CAR.matrixUnit_apply
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
matrixUnit
Used by in this Project
not_finiteDimensional_range_rootCorner
matrixUnit_mul_of_ne
MathlibAnnex.CStarAlgebra.CAR.matrixUnit_mul_of_ne
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
matrixUnit
Used by in this Project
limitMatrixUnit_mul
matrixUnit_mul_same
MathlibAnnex.CStarAlgebra.CAR.matrixUnit_mul_same
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
matrixUnit
Used by in this Project
limitMatrixUnit_mul
norm_stageTraceLinear_le
MathlibAnnex.CStarAlgebra.CAR.norm_stageTraceLinear_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageTraceLinear
Used by in this Project
stageTrace
rootFunctional
MathlibAnnex.CStarAlgebra.CAR.rootFunctional
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
rootLinear
Used by in this Project
eq_rootFunctional_of_apply_rootProjection_eq_one, rootFunctional_apply, rootFunctional_mem_stateSpaceShow 1 more
rootLinear_nonneg
MathlibAnnex.CStarAlgebra.CAR.rootLinear_nonneg
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootLinear
Used by in this Project
preRootFunctional_star_mul_self_nonneg, rootPositiveFunctional
rootProjection_mul_mul
MathlibAnnex.CStarAlgebra.CAR.rootProjection_mul_mul
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootProjection
Used by in this Project
isStarProjection_rootProjection, rootFlag_mul_ofStage_mul
stageSeparableSpace
MathlibAnnex.CStarAlgebra.CAR.stageSeparableSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageFiniteDimensional
Used by in this Project
preSeparableSpace
stage_eq_sum_smul_matrixUnit
MathlibAnnex.CStarAlgebra.CAR.stage_eq_sum_smul_matrixUnit
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
matrixUnit
Used by in this Project
ofStage_eq_sum_smul_limitMatrixUnit
star_matrixUnit
MathlibAnnex.CStarAlgebra.CAR.star_matrixUnit
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
matrixUnit
Used by in this Project
star_limitMatrixUnit
step
MathlibAnnex.CStarAlgebra.CAR.step
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
amplify, stepIndexEquiv
Used by in this Project
embed, rootFunctional_step, stageTrace_stepShow 1 more
sum_matrixUnit_diag
MathlibAnnex.CStarAlgebra.CAR.sum_matrixUnit_diag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
matrixUnit
Used by in this Project
sum_limitMatrixUnit_diag
SelectedGNS
MathlibAnnex.CStarAlgebra.PureState.SelectedGNS
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
IsPureState
Used by in this Project
SelectedAtomicHilbert, selectedRepresentation, selectedVector
positiveLinearMapOfMemStateSpace_one
MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
positiveLinearMapOfMemStateSpace
Used by in this Project
hasInnerIntertwiningSequence_of_pure, isSimpleCStarAlgebra_shellFamilyTarget
Level 3
12 declarationsexists_irreducible_atomicShellModel
MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_atomicShellModel
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ambientInclusion, instIsClosed, generator_coeShow 1 more
Used by in this Project
exists_irreducible_pureAtomicShellModel
starAlgHom_ext
MathlibAnnex.CStarAlgebra.AtomicConstruction.starAlgHom_ext
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
eq_top_of_source_mem_of_generator_mem
Used by in this Project
intertwines_of_source_of_generators
embed
MathlibAnnex.CStarAlgebra.CAR.embed
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
step
Used by in this Project
embed_refl, embed_succ
isStarProjection_rootProjection
MathlibAnnex.CStarAlgebra.CAR.isStarProjection_rootProjection
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootProjection_mul_mul
Used by in this Project
eq_rootFunctional_of_apply_rootProjection_eq_one, isStarProjection_rootFlag, step_rootProjection_mul
rootFunctional_apply
MathlibAnnex.CStarAlgebra.CAR.rootFunctional_apply
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootFunctional
Used by in this Project
rootState_rootFlag, step_rootProjection_mul
rootFunctional_step
MathlibAnnex.CStarAlgebra.CAR.rootFunctional_step
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootFunctional, step
Used by in this Project
rootFunctional_embed, step_rootProjection_mul
rootPositiveFunctional
MathlibAnnex.CStarAlgebra.CAR.rootPositiveFunctional
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
rootLinear_nonneg
Used by in this Project
rootPositiveFunctional_one
stageTrace
MathlibAnnex.CStarAlgebra.CAR.stageTrace
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
norm_stageTraceLinear_le
Used by in this Project
norm_stageTrace_le, stageTrace_apply, stageTrace_mul_commShow 1 more
step_injective
MathlibAnnex.CStarAlgebra.CAR.step_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
amplify_injective, step
Used by in this Project
norm_step
SelectedAtomicHilbert
MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
SelectedGNS
Used by in this Project
selectedAtomicRepresentation, selectedEmbedding
selectedRepresentation
MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
SelectedGNS
Used by in this Project
selectedAtomicRepresentation, selectedRootRepresentation_injective, no_unitaryIntertwiner_selectedRepresentationShow 1 more
selectedVector
MathlibAnnex.CStarAlgebra.PureState.selectedVector
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
SelectedGNS
Used by in this Project
norm_selectedVector, selected_vectorFunctional
Level 4
15 declarationsintertwines_of_source_of_generators
MathlibAnnex.CStarAlgebra.AtomicConstruction.intertwines_of_source_of_generators
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
starAlgHom_ext
Used by in this Project
exists_pointed_unitary_of_trace_of_cyclic
embed_refl
MathlibAnnex.CStarAlgebra.CAR.embed_refl
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
embed
Used by in this Project
embed_apply, rootFunctional_embed, stageTrace_embedShow 1 more
embed_succ
MathlibAnnex.CStarAlgebra.CAR.embed_succ
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
embed
Used by in this Project
embed_apply, rootFunctional_embed, stageTrace_embedShow 1 more
eq_rootFunctional_of_apply_rootProjection_eq_one
MathlibAnnex.CStarAlgebra.CAR.eq_rootFunctional_of_apply_rootProjection_eq_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_rootProjection, rootFunctional, stateSpace
Used by in this Project
isPureState_rootFunctional
norm_stageTrace_le
MathlibAnnex.CStarAlgebra.CAR.norm_stageTrace_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageTrace
Used by in this Project
norm_preTraceLinear_le
norm_step
MathlibAnnex.CStarAlgebra.CAR.norm_step
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
step_injective
Used by in this Project
isometry_step
rootPositiveFunctional_one
MathlibAnnex.CStarAlgebra.CAR.rootPositiveFunctional_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootPositiveFunctional
Used by in this Project
rootFunctional_mem_stateSpace, rootState_one
stageTrace_apply
MathlibAnnex.CStarAlgebra.CAR.stageTrace_apply
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageTrace
Used by in this Project
stageTrace_one, stageTrace_star_mul_self_nonneg, stageTrace_step
stageTrace_mul_comm
MathlibAnnex.CStarAlgebra.CAR.stageTrace_mul_comm
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageTrace
Used by in this Project
trace_mul_comm
stageTrace_rootProjection
MathlibAnnex.CStarAlgebra.CAR.stageTrace_rootProjection
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootProjection, stageTrace
Used by in this Project
trace_rootFlag
step_rootProjection_mul
MathlibAnnex.CStarAlgebra.CAR.step_rootProjection_mul
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_rootProjection, rootFunctional_apply, rootFunctional_step
Used by in this Project
rootFlag_succ_le
no_unitaryIntertwiner_selectedRepresentation
MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
selectedRepresentation
Used by in this Project
exists_irreducible_pureAtomicShellModel, isOrtho_cyclicSubspace_of_selectedStates, selected_commonFixedProjection_eq_zero
norm_selectedVector
MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
selectedVector
Used by in this Project
selectedVector_fixed_transportedFlag, instNontrivial, isIrreducible_selectedRepresentation
selectedEmbedding
MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
SelectedAtomicHilbert
Used by in this Project
exists_irreducible_pureAtomicShellModel, exists_selectedAtomicCyclicIsometry, iInf_range_atomic_transportedFlag_eq_span
selected_vectorFunctional
MathlibAnnex.CStarAlgebra.PureState.selected_vectorFunctional
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
selectedRepresentation, selectedVector
Used by in this Project
exists_selectedCyclicUnitary, selectedVector_fixed_transportedFlag, isIrreducible_selectedRepresentation
Level 5
9 declarationsembed_apply
MathlibAnnex.CStarAlgebra.CAR.embed_apply
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
embed_refl, embed_succ
Used by in this Project
embed_trans
isometry_step
MathlibAnnex.CStarAlgebra.CAR.isometry_step
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
norm_step
Used by in this Project
isometry_stage
rootFunctional_embed
MathlibAnnex.CStarAlgebra.CAR.rootFunctional_embed
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
embed_refl, embed_succ, rootFunctional_step
Used by in this Project
algRootLinear
rootFunctional_mem_stateSpace
MathlibAnnex.CStarAlgebra.CAR.rootFunctional_mem_stateSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootFunctional, rootPositiveFunctional_one, stateSpace
Used by in this Project
isPureState_rootFunctional
stageTrace_one
MathlibAnnex.CStarAlgebra.CAR.stageTrace_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageTrace_apply
Used by in this Project
trace_one
stageTrace_star_mul_self_nonneg
MathlibAnnex.CStarAlgebra.CAR.stageTrace_star_mul_self_nonneg
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageTrace_apply
Used by in this Project
trace_star_mul_self_nonneg
stageTrace_step
MathlibAnnex.CStarAlgebra.CAR.stageTrace_step
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageTrace_apply, step
Used by in this Project
stageTrace_embed
instNontrivial
MathlibAnnex.CStarAlgebra.PureState.SelectedGNS.instNontrivial
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
norm_selectedVector
Used by in this Project
exists_irreducible_pureAtomicShellModel, selectedRootRepresentation_injective, selected_commonFixedProjection_eq_zero
isIrreducible_selectedRepresentation
MathlibAnnex.CStarAlgebra.PureState.isIrreducible_selectedRepresentation
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
norm_selectedVector, selected_vectorFunctional
Used by in this Project
exists_irreducible_pureAtomicShellModel, selected_commonFixedProjection_eq_zero
Level 6
5 declarationsexists_irreducible_pureAtomicShellModel
MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_pureAtomicShellModel
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_irreducible_atomicShellModel, instNontrivial, isIrreducible_selectedRepresentation
Used by in this Project
exists_completedAtomicShellModel
embed_trans
MathlibAnnex.CStarAlgebra.CAR.embed_trans
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
embed_apply
Used by in this Project
embedDirectedSystem
isPureState_rootFunctional
MathlibAnnex.CStarAlgebra.CAR.isPureState_rootFunctional
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
eq_rootFunctional_of_apply_rootProjection_eq_one, rootFunctional_mem_stateSpace, IsPureState
Used by in this Project
isPureState_rootState
isometry_stage
MathlibAnnex.CStarAlgebra.CAR.isometry_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isometry_step
Used by in this Project
PreCAR
stageTrace_embed
MathlibAnnex.CStarAlgebra.CAR.stageTrace_embed
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
embed_refl, embed_succ, stageTrace_step
Used by in this Project
algTraceLinear
Level 7
2 declarationsPreCAR
MathlibAnnex.CStarAlgebra.CAR.PreCAR
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
isometry_stage
embedDirectedSystem
MathlibAnnex.CStarAlgebra.CAR.embedDirectedSystem
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
embed_trans
Used by in this Project
AlgCAR
Level 8
2 declarationsAlgCAR
MathlibAnnex.CStarAlgebra.CAR.AlgCAR
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
embedDirectedSystem
Used by in this Project
algRootLinear, algStageHom, algToPreShow 2 more
toPreCAR
MathlibAnnex.CStarAlgebra.CAR.toPreCAR
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
PreCAR
Used by in this Project
isometry_toPreCAR, toPreCAR_step
Level 9
6 declarationsalgRootLinear
MathlibAnnex.CStarAlgebra.CAR.algRootLinear
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
AlgCAR, rootFunctional_embed
Used by in this Project
preRootLinear
algStageHom
MathlibAnnex.CStarAlgebra.CAR.algStageHom
Exact source-authored def in the Naimark construction.
algTraceLinear
MathlibAnnex.CStarAlgebra.CAR.algTraceLinear
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
AlgCAR, stageTrace_embed
Used by in this Project
preTraceLinear
isometry_toPreCAR
MathlibAnnex.CStarAlgebra.CAR.isometry_toPreCAR
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
toPreCAR
Used by in this Project
norm_stageHom, stageHom_injective
preToAlg
MathlibAnnex.CStarAlgebra.CAR.preToAlg
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
AlgCAR, PreCAR
Used by in this Project
algToPre_preToAlg, preToAlg_algToPre
toPreCAR_step
MathlibAnnex.CStarAlgebra.CAR.toPreCAR_step
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
toPreCAR
Used by in this Project
toPreCAR_embed
Level 10
1 declarationtoPreCAR_embed
MathlibAnnex.CStarAlgebra.CAR.toPreCAR_embed
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
embed_refl, embed_succ, toPreCAR_step
Used by in this Project
algToPre
Level 11
1 declarationalgToPre
MathlibAnnex.CStarAlgebra.CAR.algToPre
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
AlgCAR, toPreCAR_embed
Used by in this Project
algToPre_preToAlg, preToAlg_algToPre
Level 12
2 declarationsalgToPre_preToAlg
MathlibAnnex.CStarAlgebra.CAR.algToPre_preToAlg
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
algToPre, preToAlg
Used by in this Project
preAlgEquiv
preToAlg_algToPre
MathlibAnnex.CStarAlgebra.CAR.preToAlg_algToPre
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
algToPre, preToAlg
Used by in this Project
preAlgEquiv
Level 13
1 declarationpreAlgEquiv
MathlibAnnex.CStarAlgebra.CAR.preAlgEquiv
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
algToPre_preToAlg, preToAlg_algToPre
Used by in this Project
preRing
Level 14
1 declarationpreRing
MathlibAnnex.CStarAlgebra.CAR.preRing
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
preAlgEquiv
Used by in this Project
preAlgebra, preNorm, preStarRing
Level 15
3 declarationspreAlgebra
MathlibAnnex.CStarAlgebra.CAR.preAlgebra
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
preRing
Used by in this Project
preStarAlgEquiv, preStarModule
preNorm
MathlibAnnex.CStarAlgebra.CAR.preNorm
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
preRing
Used by in this Project
norm_stageHom
preStarRing
MathlibAnnex.CStarAlgebra.CAR.preStarRing
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
preRing
Used by in this Project
preStarAlgEquiv, preStarModule
Level 16
2 declarationspreStarAlgEquiv
MathlibAnnex.CStarAlgebra.CAR.preStarAlgEquiv
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
preAlgebra, preStarRing
Used by in this Project
stageHom
preStarModule
MathlibAnnex.CStarAlgebra.CAR.preStarModule
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
preAlgebra, preStarRing
Used by in this Project
limitStarModule
Level 17
1 declarationstageHom
MathlibAnnex.CStarAlgebra.CAR.stageHom
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
algStageHom, preStarAlgEquiv
Used by in this Project
exists_common_stage, stageHom_apply
Level 18
2 declarationsexists_common_stage
MathlibAnnex.CStarAlgebra.CAR.exists_common_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageHom
Used by in this Project
preNormedAddCommGroup
stageHom_apply
MathlibAnnex.CStarAlgebra.CAR.stageHom_apply
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageHom
Used by in this Project
norm_stageHom, stageHom_injective
Level 19
2 declarationsnorm_stageHom
MathlibAnnex.CStarAlgebra.CAR.norm_stageHom
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isometry_toPreCAR, preNorm, stageHom_apply
Used by in this Project
preNormedAddCommGroup
stageHom_injective
MathlibAnnex.CStarAlgebra.CAR.stageHom_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isometry_toPreCAR, stageHom_apply
Used by in this Project
preNontrivial
Level 20
2 declarationspreNontrivial
MathlibAnnex.CStarAlgebra.CAR.preNontrivial
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageHom_injective, stageNontrivial
Used by in this Project
limitNontrivial
preNormedAddCommGroup
MathlibAnnex.CStarAlgebra.CAR.preNormedAddCommGroup
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
exists_common_stage, norm_stageHom
Used by in this Project
preNormedRing
Level 21
1 declarationpreNormedRing
MathlibAnnex.CStarAlgebra.CAR.preNormedRing
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
preNormedAddCommGroup
Used by in this Project
Limit, dense_stageUnion, preCStarRingShow 2 more
Level 22
5 declarationsLimit
MathlibAnnex.CStarAlgebra.CAR.Limit
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
preNormedRing
Used by in this Project
limitNontrivial, limitNormedAlgebra, limitSeparableSpace
dense_stageUnion
MathlibAnnex.CStarAlgebra.CAR.dense_stageUnion
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
preNormedRing
Used by in this Project
dense_stageRange
preCStarRing
MathlibAnnex.CStarAlgebra.CAR.preCStarRing
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
preNormedRing
Used by in this Project
star_coe
preNormedSpace
MathlibAnnex.CStarAlgebra.CAR.preNormedSpace
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
preNormedRing
Used by in this Project
AlternatingState, HasInnerIntertwiningSequence, innerAtShow 6 more
preSeparableSpace
MathlibAnnex.CStarAlgebra.CAR.preSeparableSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
preNormedRing, stageSeparableSpace
Used by in this Project
limitSeparableSpace
Level 23
7 declarationslimitNontrivial
MathlibAnnex.CStarAlgebra.CAR.limitNontrivial
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
Limit, preNontrivial
Used by in this Project
limitIsSimpleRing, norm_rowAverageLinear_le
limitNormedAlgebra
MathlibAnnex.CStarAlgebra.CAR.limitNormedAlgebra
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
Limit, preNormedSpace
Used by in this Project
cornerExponential, limitCStarAlgebra
limitSeparableSpace
MathlibAnnex.CStarAlgebra.CAR.limitSeparableSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
Limit, preSeparableSpace
Used by in this Project
separableSpace_traceHilbertSpace, transportDense
limitStar
MathlibAnnex.CStarAlgebra.CAR.limitStar
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
Limit
Used by in this Project
AlternatingState, continuous_limit_star, star_coe
preNormedAlgebra
MathlibAnnex.CStarAlgebra.CAR.preNormedAlgebra
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
preNormedSpace
Used by in this Project
liftedCornerExponentialPath, rootState_nonneg, trace_nonneg
preRootLinear
MathlibAnnex.CStarAlgebra.CAR.preRootLinear
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
algRootLinear, preNormedSpace
Used by in this Project
preRootLinear_stage
preTraceLinear
MathlibAnnex.CStarAlgebra.CAR.preTraceLinear
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
algTraceLinear, preNormedSpace
Used by in this Project
preTraceLinear_stageHom
Level 24
6 declarationsAlternatingState
MathlibAnnex.CStarAlgebra.CAR.AlternatingState
Exact source-authored inductive in the Naimark construction.
Immediate prerequisites in this Project
limitStar, preNormedSpace
Used by in this Project
AlternatingTransition, nonempty_initialState
continuous_limit_star
MathlibAnnex.CStarAlgebra.CAR.continuous_limit_star
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitStar
Used by in this Project
limitContinuousStar, limitStarModule, rootState_star_mul_self_nonnegShow 1 more
preRootLinear_stage
MathlibAnnex.CStarAlgebra.CAR.preRootLinear_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
preRootLinear
Used by in this Project
norm_preRootLinear_le
preTraceLinear_stageHom
MathlibAnnex.CStarAlgebra.CAR.preTraceLinear_stageHom
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
preTraceLinear
Used by in this Project
norm_preTraceLinear_le
star_coe
MathlibAnnex.CStarAlgebra.CAR.star_coe
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitStar, preCStarRing
Used by in this Project
limitStarModule, limitStarRing, rootState_star_mul_self_nonnegShow 2 more
transportDense
MathlibAnnex.CStarAlgebra.CAR.transportDense
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitSeparableSpace
Used by in this Project
densePrefix, denseRange_transportDense
Level 25
8 declarationsAlternatingTransition
MathlibAnnex.CStarAlgebra.CAR.AlternatingTransition
Exact source-authored inductive in the Naimark construction.
Immediate prerequisites in this Project
AlternatingState
Used by in this Project
nonempty_transition
densePrefix
MathlibAnnex.CStarAlgebra.CAR.densePrefix
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
transportDense
Used by in this Project
mem_densePrefix, protectedPrefix
denseRange_transportDense
MathlibAnnex.CStarAlgebra.CAR.denseRange_transportDense
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
transportDense
Used by in this Project
leftAutomorphisms_cauchy, leftAutomorphisms_symm_cauchy, rightAutomorphisms_cauchy
limitContinuousStar
MathlibAnnex.CStarAlgebra.CAR.limitContinuousStar
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
continuous_limit_star
Used by in this Project
limitStarRing
limitStarModule
MathlibAnnex.CStarAlgebra.CAR.limitStarModule
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
continuous_limit_star, preNormedSpace, preStarModuleShow 1 more
Used by in this Project
cornerExponential, limitCStarAlgebra
norm_preRootLinear_le
MathlibAnnex.CStarAlgebra.CAR.norm_preRootLinear_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
preRootLinear_stage
Used by in this Project
preRootFunctional
norm_preTraceLinear_le
MathlibAnnex.CStarAlgebra.CAR.norm_preTraceLinear_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
norm_stageTrace_le, preTraceLinear_stageHom
Used by in this Project
preTrace
toLimit
MathlibAnnex.CStarAlgebra.CAR.toLimit
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
preNormedSpace, star_coe
Used by in this Project
ofStage
Level 26
5 declarationslimitStarRing
MathlibAnnex.CStarAlgebra.CAR.limitStarRing
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitContinuousStar, star_coe
Used by in this Project
HasInnerIntertwiningSequence, cornerExponential, innerAtShow 2 more
mem_densePrefix
MathlibAnnex.CStarAlgebra.CAR.mem_densePrefix
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
densePrefix
Used by in this Project
mem_protectedPrefix, mem_symm_protectedPrefix, nonempty_transition
ofStage
MathlibAnnex.CStarAlgebra.CAR.ofStage
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
toLimit
Used by in this Project
dense_stageRange, limitMatrixUnit, ofStage_applyShow 3 more
preRootFunctional
MathlibAnnex.CStarAlgebra.CAR.preRootFunctional
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
norm_preRootLinear_le
Used by in this Project
preRootFunctional_stage, rootState
preTrace
MathlibAnnex.CStarAlgebra.CAR.preTrace
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
norm_preTraceLinear_le
Used by in this Project
preTrace_stageHom, trace
Level 27
13 declarationsHasInnerIntertwiningSequence
MathlibAnnex.CStarAlgebra.CAR.HasInnerIntertwiningSequence
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitStarRing, preNormedSpace
Used by in this Project
hasInnerIntertwiningSequence_vectorFunctional, homogeneity_of_innerIntertwiningSequences
dense_stageRange
MathlibAnnex.CStarAlgebra.CAR.dense_stageRange
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
dense_stageUnion, ofStage
Used by in this Project
eq_rootState_of_restrict, eq_trace_of_apply_one_of_mul_comm, exists_stage_approxShow 2 more
innerAt
MathlibAnnex.CStarAlgebra.CAR.innerAt
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitStarRing, preNormedSpace
Used by in this Project
protectedPrefix
limitCStarRing
MathlibAnnex.CStarAlgebra.CAR.limitCStarRing
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitStarRing
Used by in this Project
limitCStarAlgebra
limitMatrixUnit
MathlibAnnex.CStarAlgebra.CAR.limitMatrixUnit
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
matrixUnit, ofStage
Used by in this Project
IsRootCornerUnitary, cornerExponential, cornerLift
ofStage_apply
MathlibAnnex.CStarAlgebra.CAR.ofStage_apply
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ofStage
Used by in this Project
norm_ofStage, rootState_stage, trace_ofStage
ofStage_embed
MathlibAnnex.CStarAlgebra.CAR.ofStage_embed
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ofStage
Used by in this Project
exists_common_stage_approx, rootFlag_mul_ofStage_mul
ofStage_step
MathlibAnnex.CStarAlgebra.CAR.ofStage_step
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ofStage
Used by in this Project
rootFlag_succ_le
preRootFunctional_stage
MathlibAnnex.CStarAlgebra.CAR.preRootFunctional_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
preRootFunctional
Used by in this Project
preRootFunctional_star_mul_self_nonneg, rootState_stage
preTrace_stageHom
MathlibAnnex.CStarAlgebra.CAR.preTrace_stageHom
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
preTrace
Used by in this Project
trace_mul_comm, trace_ofStage, trace_star_mul_self_nonneg
rootFlag
MathlibAnnex.CStarAlgebra.CAR.rootFlag
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
ofStage, rootProjection
Used by in this Project
compressionError, isStarProjection_rootFlag, representedRootFlag
rootState
MathlibAnnex.CStarAlgebra.CAR.rootState
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
Limit, preRootFunctional
Used by in this Project
compressionError, rootState_coe
trace
MathlibAnnex.CStarAlgebra.CAR.trace
Exact source-authored def in the Naimark construction.
Level 28
20 declarationsIsRootCornerUnitary
MathlibAnnex.CStarAlgebra.CAR.IsRootCornerUnitary
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit
Used by in this Project
cornerLift_mem_unitary, isRootCornerUnitary_cornerExponential
compressionError
MathlibAnnex.CStarAlgebra.CAR.compressionError
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
rootFlag, rootState
Used by in this Project
compressionError_ofStage, compressionError_sub, norm_compressionError_le
cornerExponential
MathlibAnnex.CStarAlgebra.CAR.cornerExponential
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit, limitNormedAlgebra, limitStarModuleShow 1 more
Used by in this Project
exists_rootCornerSupported_exponential_eq_on, isRootCornerUnitary_cornerExponential
cornerLift
MathlibAnnex.CStarAlgebra.CAR.cornerLift
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit
Used by in this Project
cornerLift_eq_rowAverageLinear, representation_cornerLift_apply, star_cornerLift
isStarProjection_rootFlag
MathlibAnnex.CStarAlgebra.CAR.isStarProjection_rootFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_rootProjection, rootFlag
Used by in this Project
instHasOrthogonalProjectionRepresentedRootFlag, isStarProjection_transportedFlag, norm_compressionError_leShow 2 more
limitCStarAlgebra
MathlibAnnex.CStarAlgebra.CAR.limitCStarAlgebra
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitCStarRing, limitNormedAlgebra, limitStarModule
Used by in this Project
exists_rootCornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on, exists_stage_approx, limitPartialOrder
limitMatrixUnit_mul
MathlibAnnex.CStarAlgebra.CAR.limitMatrixUnit_mul
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit, matrixUnit_mul_of_ne, matrixUnit_mul_same
Used by in this Project
apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm, cornerLift_mem_unitary, isRootCornerUnitary_cornerExponential
norm_ofStage
MathlibAnnex.CStarAlgebra.CAR.norm_ofStage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ofStage_apply
Used by in this Project
norm_rootRepresentation_stage, ofStage_injective, restrictState
preRootFunctional_star_mul_self_nonneg
MathlibAnnex.CStarAlgebra.CAR.preRootFunctional_star_mul_self_nonneg
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
preRootFunctional_stage, rootLinear_nonneg
Used by in this Project
rootState_star_mul_self_nonneg
protectedPrefix
MathlibAnnex.CStarAlgebra.CAR.protectedPrefix
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
densePrefix, innerAt
Used by in this Project
mem_protectedPrefix, mem_symm_protectedPrefix, nonempty_initialStateShow 1 more
reconstructedStageVector
MathlibAnnex.CStarAlgebra.CAR.reconstructedStageVector
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit
Used by in this Project
representation_matrixUnit_reconstructedStageVector
rootCornerSubspace
MathlibAnnex.CStarAlgebra.CAR.rootCornerSubspace
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit
Used by in this Project
exists_rootCornerSupported_exponential_apply_eq_involution
rootFlag_zero
MathlibAnnex.CStarAlgebra.CAR.rootFlag_zero
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootFlag
Used by in this Project
transportedFlag_zero
rootShell
MathlibAnnex.CStarAlgebra.CAR.rootShell
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
rootFlag
Used by in this Project
isStarProjection_rootShell, representativeLink_final, representativeLink_initialShow 1 more
rootState_coe
MathlibAnnex.CStarAlgebra.CAR.rootState_coe
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootState
Used by in this Project
rootState_stage, rootState_star_mul_self_nonneg
rowAverageLinear
MathlibAnnex.CStarAlgebra.CAR.rowAverageLinear
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit
Used by in this Project
cornerLift_eq_rowAverageLinear, rowAverageLinear_apply, rowAverageLinear_one
stageTests
MathlibAnnex.CStarAlgebra.CAR.stageTests
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit
Used by in this Project
mem_stageTests
star_limitMatrixUnit
MathlibAnnex.CStarAlgebra.CAR.star_limitMatrixUnit
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit, star_matrixUnit
Used by in this Project
isRootCornerUnitary_cornerExponential, isStarProjection_limitMatrixUnit_zero_zero, rowAverageLinear_nonneg
sum_limitMatrixUnit_diag
MathlibAnnex.CStarAlgebra.CAR.sum_limitMatrixUnit_diag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit, sum_matrixUnit_diag
Used by in this Project
apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm, cornerLift_mem_unitary, rowAverageLinear_oneShow 1 more
trace_coe
MathlibAnnex.CStarAlgebra.CAR.trace_coe
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
trace
Used by in this Project
norm_trace_le, trace_mul_comm, trace_ofStageShow 1 more
Level 29
24 declarationscompressionError_sub
MathlibAnnex.CStarAlgebra.CAR.compressionError_sub
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
compressionError
Used by in this Project
tendsto_norm_compressionError
cornerLift_eq_rowAverageLinear
MathlibAnnex.CStarAlgebra.CAR.cornerLift_eq_rowAverageLinear
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
cornerLift, rowAverageLinear
Used by in this Project
ofStage_commute_cornerLift
exists_stage_approx
MathlibAnnex.CStarAlgebra.CAR.exists_stage_approx
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
dense_stageRange, limitCStarAlgebra
Used by in this Project
exists_common_stage_approx
isRootCornerUnitary_cornerExponential
MathlibAnnex.CStarAlgebra.CAR.isRootCornerUnitary_cornerExponential
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
IsRootCornerUnitary, cornerExponential, limitMatrixUnit_mulShow 1 more
Used by in this Project
liftedCornerExponential
isStarProjection_limitMatrixUnit_zero_zero
MathlibAnnex.CStarAlgebra.CAR.isStarProjection_limitMatrixUnit_zero_zero
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit_mul, star_limitMatrixUnit
Used by in this Project
exists_rootCornerFamily_with_gram, exists_rootCornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on
limitPartialOrder
MathlibAnnex.CStarAlgebra.CAR.limitPartialOrder
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitCStarAlgebra
Used by in this Project
limitStarOrderedRing
mem_protectedPrefix
MathlibAnnex.CStarAlgebra.CAR.mem_protectedPrefix
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
mem_densePrefix, protectedPrefix
Used by in this Project
leftAutomorphisms_step, rightAutomorphisms_step
mem_stageTests
MathlibAnnex.CStarAlgebra.CAR.mem_stageTests
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageTests
Used by in this Project
nonempty_initialState, nonempty_transition
mem_symm_protectedPrefix
MathlibAnnex.CStarAlgebra.CAR.mem_symm_protectedPrefix
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
mem_densePrefix, protectedPrefix
Used by in this Project
leftAutomorphisms_symm_step, rightAutomorphisms_symm_step
norm_compressionError_le
MathlibAnnex.CStarAlgebra.CAR.norm_compressionError_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
compressionError, isStarProjection_rootFlag, limitCStarAlgebra
Used by in this Project
tendsto_norm_compressionError
norm_trace_le
MathlibAnnex.CStarAlgebra.CAR.norm_trace_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitCStarAlgebra, trace_coe
Used by in this Project
exists_state_extension_trace
ofStage_injective
MathlibAnnex.CStarAlgebra.CAR.ofStage_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitCStarAlgebra, norm_ofStage
Used by in this Project
not_finiteDimensional
representation_cornerLift_apply
MathlibAnnex.CStarAlgebra.CAR.representation_cornerLift_apply
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
cornerLift
Used by in this Project
representation_liftedCornerExponential_apply_of_root
representation_matrixUnit_reconstructedStageVector
MathlibAnnex.CStarAlgebra.CAR.representation_matrixUnit_reconstructedStageVector
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit_mul, reconstructedStageVector
Used by in this Project
vectorFunctional_reconstructedStageVector_matrixUnit
restrictState
MathlibAnnex.CStarAlgebra.CAR.restrictState
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitCStarAlgebra, norm_ofStage
Used by in this Project
eq_rootState_of_restrict, restrictState_apply
rootState_stage
MathlibAnnex.CStarAlgebra.CAR.rootState_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ofStage_apply, preRootFunctional_stage, rootState_coe
Used by in this Project
eq_rootState_of_restrict, rootFlag_mul_ofStage_mul, rootState_oneShow 1 more
rootState_star_mul_self_nonneg
MathlibAnnex.CStarAlgebra.CAR.rootState_star_mul_self_nonneg
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
continuous_limit_star, preRootFunctional_star_mul_self_nonneg, rootState_coeShow 1 more
Used by in this Project
rootState_nonneg
rowAverageLinear_apply
MathlibAnnex.CStarAlgebra.CAR.rowAverageLinear_apply
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rowAverageLinear
Used by in this Project
limitMatrixUnit_commute_rowAverage, rowAverageLinear_nonneg
rowAverageLinear_one
MathlibAnnex.CStarAlgebra.CAR.rowAverageLinear_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit_mul, rowAverageLinear, sum_limitMatrixUnit_diag
Used by in this Project
norm_rowAverageLinear_le
row_isometry_sum
MathlibAnnex.CStarAlgebra.CAR.row_isometry_sum
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit_mul, star_limitMatrixUnit, sum_limitMatrixUnit_diag
Used by in this Project
sum_norm_sq_map_limitMatrixUnit_star
star_cornerLift
MathlibAnnex.CStarAlgebra.CAR.star_cornerLift
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
cornerLift, limitStarRing, star_limitMatrixUnit
Used by in this Project
cornerLift_mem_unitary
trace_mul_comm
MathlibAnnex.CStarAlgebra.CAR.trace_mul_comm
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitCStarAlgebra, preTrace_stageHom, stageTrace_mul_commShow 1 more
Used by in this Project
apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm, tendsto_rootFlag_orbit_zero, trace_transportedFlag_eq_trace_rootFlag
trace_ofStage
MathlibAnnex.CStarAlgebra.CAR.trace_ofStage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ofStage_apply, preTrace_stageHom, trace_coe
Used by in this Project
trace_one, trace_rootFlag
trace_star_mul_self_nonneg
MathlibAnnex.CStarAlgebra.CAR.trace_star_mul_self_nonneg
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
continuous_limit_star, preTrace_stageHom, stageTrace_star_mul_self_nonneg
Used by in this Project
trace_nonneg
Level 30
12 declarationscornerLift_mem_unitary
MathlibAnnex.CStarAlgebra.CAR.cornerLift_mem_unitary
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
IsRootCornerUnitary, limitMatrixUnit_mul, star_cornerLiftShow 1 more
Used by in this Project
liftedCornerExponential
eq_rootState_of_restrict
MathlibAnnex.CStarAlgebra.CAR.eq_rootState_of_restrict
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
dense_stageRange, restrictState, rootState_stage
Used by in this Project
isPureState_rootState
exists_common_stage_approx
MathlibAnnex.CStarAlgebra.CAR.exists_common_stage_approx
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_stage_approx, ofStage_embed
Used by in this Project
exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt, exists_unitary_crossRepresentation_path_approx
exists_rootCornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on
MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_limitMatrixUnit_zero_zero, limitCStarAlgebra
Used by in this Project
exists_rootCornerSupported_exponential_eq_on
limitMatrixUnit_commute_rowAverage
MathlibAnnex.CStarAlgebra.CAR.limitMatrixUnit_commute_rowAverage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit_mul, rowAverageLinear_apply
Used by in this Project
ofStage_commute_rowAverage
limitStarOrderedRing
MathlibAnnex.CStarAlgebra.CAR.limitStarOrderedRing
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitPartialOrder
Used by in this Project
PureStateHomogeneity, RepresentativeShellData, ofStage_eq_sum_smul_limitMatrixUnit
not_finiteDimensional
MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
finrank_stage, ofStage_injective
Used by in this Project
eq_zero_of_isCompactOperator_image, not_finiteDimensional_shellFamilyTarget
restrictState_apply
MathlibAnnex.CStarAlgebra.CAR.restrictState_apply
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
restrictState
Used by in this Project
restrictState_mem_stateSpace
rootState_one
MathlibAnnex.CStarAlgebra.CAR.rootState_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootPositiveFunctional_one, rootState_stage
Used by in this Project
rootPositiveState_one, rootState_mem_stateSpace
rootState_rootFlag
MathlibAnnex.CStarAlgebra.CAR.rootState_rootFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootFlag, rootFunctional_apply, rootState_stage
Used by in this Project
exists_selectedAtomicCyclicIsometry, selectedVector_fixed_transportedFlag
trace_one
MathlibAnnex.CStarAlgebra.CAR.trace_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
stageTrace_one, trace_ofStage
Used by in this Project
apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm, exists_state_extension_trace, tracePositive_one
trace_rootFlag
MathlibAnnex.CStarAlgebra.CAR.trace_rootFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootFlag, stageTrace_rootProjection, trace_ofStage
Used by in this Project
tendsto_rootFlag_orbit_zero, trace_transportedFlag
Level 31
14 declarationsPureStateHomogeneity
MathlibAnnex.CStarAlgebra.CAR.PureStateHomogeneity
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
limitStarOrderedRing, IsPureState
Used by in this Project
homogeneity_of_innerIntertwiningSequences
RepresentativeShellData
MathlibAnnex.CStarAlgebra.CAR.RepresentativeShellData
Exact source-authored inductive in the Naimark construction.
Immediate prerequisites in this Project
limitStarOrderedRing, IsPureState
Used by in this Project
representativeShellData, representativeShellDataOfHomogeneity
apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm
MathlibAnnex.CStarAlgebra.CAR.apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit_mul, sum_limitMatrixUnit_diag, trace_mul_commShow 1 more
Used by in this Project
apply_ofStage_eq_trace_of_apply_one_of_mul_comm
exists_rootCornerSupported_exponential_eq_on
MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerSupported_exponential_eq_on
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
cornerExponential, exists_rootCornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on
Used by in this Project
exists_rootCornerSupported_exponential_apply_eq_involution
liftedCornerExponential
MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponential
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
cornerLift_mem_unitary, isRootCornerUnitary_cornerExponential
Used by in this Project
liftedCornerExponentialPath, liftedCornerExponential_commute_stage, representation_liftedCornerExponential_apply_of_root
ofStage_eq_sum_smul_limitMatrixUnit
MathlibAnnex.CStarAlgebra.CAR.ofStage_eq_sum_smul_limitMatrixUnit
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit, limitStarOrderedRing, stage_eq_sum_smul_matrixUnit
Used by in this Project
apply_ofStage_eq_trace_of_apply_one_of_mul_comm, continuousLinearMap_eq_on_ofStage_of_eq_matrixUnit, ofStage_commute_rowAverage
restrictState_mem_stateSpace
MathlibAnnex.CStarAlgebra.CAR.restrictState_mem_stateSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitStarOrderedRing, restrictState_apply, stateSpace
Used by in this Project
isPureState_rootState
rootFlag_mul_ofStage_mul
MathlibAnnex.CStarAlgebra.CAR.rootFlag_mul_ofStage_mul
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitStarOrderedRing, ofStage_embed, rootFlagShow 2 more
Used by in this Project
compressionError_ofStage
rootFlag_succ_le
MathlibAnnex.CStarAlgebra.CAR.rootFlag_succ_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_rootFlag, limitStarOrderedRing, ofStage_stepShow 1 more
Used by in this Project
antitone_rootFlag, isStarProjection_rootShell
rootState_nonneg
MathlibAnnex.CStarAlgebra.CAR.rootState_nonneg
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitStarOrderedRing, preNormedAlgebra, rootState_star_mul_self_nonneg
Used by in this Project
rootPositiveState, rootState_mem_stateSpace
rowAverageLinear_nonneg
MathlibAnnex.CStarAlgebra.CAR.rowAverageLinear_nonneg
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitStarOrderedRing, rowAverageLinear_apply, star_limitMatrixUnit
Used by in this Project
rowAveragePositive
sum_norm_sq_map_limitMatrixUnit_star
MathlibAnnex.CStarAlgebra.CAR.sum_norm_sq_map_limitMatrixUnit_star
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitStarOrderedRing, row_isometry_sum
Used by in this Project
exists_delta_stageCentral_unitary_path_apply_sub_norm_lt
trace_nonneg
MathlibAnnex.CStarAlgebra.CAR.trace_nonneg
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitStarOrderedRing, preNormedAlgebra, trace_star_mul_self_nonneg
Used by in this Project
tracePositive
vectorFunctional_reconstructedStageVector_matrixUnit
MathlibAnnex.CStarAlgebra.CAR.vectorFunctional_reconstructedStageVector_matrixUnit
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitStarOrderedRing, representation_matrixUnit_reconstructedStageVector, star_limitMatrixUnit
Used by in this Project
reconstructedStageVector_vectorFunctional_eq_on_stage
Level 32
13 declarationsantitone_rootFlag
MathlibAnnex.CStarAlgebra.CAR.antitone_rootFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootFlag_succ_le
Used by in this Project
rootFlag_mul_of_le
apply_ofStage_eq_trace_of_apply_one_of_mul_comm
MathlibAnnex.CStarAlgebra.CAR.apply_ofStage_eq_trace_of_apply_one_of_mul_comm
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm, ofStage_eq_sum_smul_limitMatrixUnit
Used by in this Project
eq_trace_of_apply_one_of_mul_comm
compressionError_ofStage
MathlibAnnex.CStarAlgebra.CAR.compressionError_ofStage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
compressionError, rootFlag_mul_ofStage_mul
Used by in this Project
tendsto_norm_compressionError
continuousLinearMap_eq_on_ofStage_of_eq_matrixUnit
MathlibAnnex.CStarAlgebra.CAR.continuousLinearMap_eq_on_ofStage_of_eq_matrixUnit
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ofStage_eq_sum_smul_limitMatrixUnit
Used by in this Project
reconstructedStageVector_vectorFunctional_eq_on_stage
homogeneity_of_innerIntertwiningSequences
MathlibAnnex.CStarAlgebra.CAR.homogeneity_of_innerIntertwiningSequences
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
HasInnerIntertwiningSequence, PureStateHomogeneity
Used by in this Project
homogeneity
isStarProjection_rootShell
MathlibAnnex.CStarAlgebra.CAR.isStarProjection_rootShell
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootFlag_succ_le, rootShell
Used by in this Project
rootShell_mul_star_rootShell, star_rootShell_mul_rootShell
ofStage_commute_rowAverage
MathlibAnnex.CStarAlgebra.CAR.ofStage_commute_rowAverage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitMatrixUnit_commute_rowAverage, ofStage_eq_sum_smul_limitMatrixUnit
Used by in this Project
ofStage_commute_cornerLift
representation_liftedCornerExponential_apply_of_root
MathlibAnnex.CStarAlgebra.CAR.representation_liftedCornerExponential_apply_of_root
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
liftedCornerExponential, representation_cornerLift_apply
Used by in this Project
exists_liftedCornerExponential_apply_eq_involution
representativeShellData
MathlibAnnex.CStarAlgebra.CAR.representativeShellData
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
RepresentativeShellData, RepresentativeShellFamily
Used by in this Project
representativeLink_final, representativeShellData_root_alpha, representativeShellData_root_linkShow 2 more
rootPositiveState
MathlibAnnex.CStarAlgebra.CAR.rootPositiveState
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
rootState_nonneg
Used by in this Project
norm_leftMulMapPreGNS_apply_le, rootPositiveState_one
rootState_mem_stateSpace
MathlibAnnex.CStarAlgebra.CAR.rootState_mem_stateSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootState_nonneg, rootState_one, stateSpace
Used by in this Project
isPureState_rootState
rowAveragePositive
MathlibAnnex.CStarAlgebra.CAR.rowAveragePositive
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
rowAverageLinear_nonneg
Used by in this Project
norm_rowAverageLinear_le
tracePositive
MathlibAnnex.CStarAlgebra.CAR.tracePositive
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
trace_nonneg
Used by in this Project
TraceHilbertSpace, tendsto_rootFlag_orbit_zero, tendsto_transportedFlag_orbit_zeroShow 1 more
Level 33
16 declarationsTraceHilbertSpace
MathlibAnnex.CStarAlgebra.CAR.TraceHilbertSpace
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
tracePositive
Used by in this Project
SeparableCounterexampleHilbertSpace, traceRepresentation, traceVector
eq_trace_of_apply_one_of_mul_comm
MathlibAnnex.CStarAlgebra.CAR.eq_trace_of_apply_one_of_mul_comm
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
apply_ofStage_eq_trace_of_apply_one_of_mul_comm, dense_stageRange
Used by in this Project
apply_shellFamilySourceHom_eq_trace_of_apply_one_of_mul_comm
isPureState_rootState
MathlibAnnex.CStarAlgebra.CAR.isPureState_rootState
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
eq_rootState_of_restrict, isPureState_rootFunctional, restrictState_mem_stateSpaceShow 1 more
Used by in this Project
completedRootPureState
norm_leftMulMapPreGNS_apply_le
MathlibAnnex.CStarAlgebra.CAR.norm_leftMulMapPreGNS_apply_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootPositiveState
Used by in this Project
norm_rootRepresentation_le
norm_rowAverageLinear_le
MathlibAnnex.CStarAlgebra.CAR.norm_rowAverageLinear_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitNontrivial, rowAverageLinear_one, rowAveragePositive
Used by in this Project
rowAverage
ofStage_commute_cornerLift
MathlibAnnex.CStarAlgebra.CAR.ofStage_commute_cornerLift
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
cornerLift_eq_rowAverageLinear, ofStage_commute_rowAverage
Used by in this Project
liftedCornerExponential_commute_stage
reconstructedStageVector_vectorFunctional_eq_on_stage
MathlibAnnex.CStarAlgebra.CAR.reconstructedStageVector_vectorFunctional_eq_on_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
continuousLinearMap_eq_on_ofStage_of_eq_matrixUnit, vectorFunctional_reconstructedStageVector_matrixUnit
Used by in this Project
norm_reconstructedStageVector_eq_one
representativeLink_final
MathlibAnnex.CStarAlgebra.CAR.representativeLink_final
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
representativeShellData, rootShell
Used by in this Project
exists_completedAtomicShellModel, exists_targetShellReconstruction, trace_transportedFlag_eq_trace_rootFlag
rootFlag_mul_of_le
MathlibAnnex.CStarAlgebra.CAR.rootFlag_mul_of_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
antitone_rootFlag
Used by in this Project
transportedFlag_mul_of_le
rootPositiveState_one
MathlibAnnex.CStarAlgebra.CAR.rootPositiveState_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootPositiveState, rootState_one
Used by in this Project
rootGNSNontrivial
rootShell_mul_star_rootShell
MathlibAnnex.CStarAlgebra.CAR.rootShell_mul_star_rootShell
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_rootShell
Used by in this Project
rootShell_identity_family
star_rootShell_mul_rootShell
MathlibAnnex.CStarAlgebra.CAR.star_rootShell_mul_rootShell
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_rootShell
Used by in this Project
rootShell_identity_family
tendsto_norm_compressionError
MathlibAnnex.CStarAlgebra.CAR.tendsto_norm_compressionError
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
compressionError_ofStage, compressionError_sub, dense_stageRangeShow 1 more
Used by in this Project
exists_rootFlag_mem_of_ne_zero_mem, tendsto_norm_transported_compressionError
tendsto_rootFlag_orbit_zero
MathlibAnnex.CStarAlgebra.CAR.tendsto_rootFlag_orbit_zero
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_rootFlag, tracePositive, trace_mul_commShow 1 more
Used by in this Project
exists_shell_sums_eq_on_cyclicSubspace
tracePositive_one
MathlibAnnex.CStarAlgebra.CAR.tracePositive_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
tracePositive, trace_one
Used by in this Project
norm_traceVector
transportedFlag
MathlibAnnex.CStarAlgebra.CAR.transportedFlag
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
representativeShellData, rootFlag
Used by in this Project
isStarProjection_transportedFlag, representativeLink_initial, representedGenerator_comp_sourceShell
Level 34
14 declarationsSeparableCounterexampleHilbertSpace
MathlibAnnex.CStarAlgebra.CAR.SeparableCounterexampleHilbertSpace
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
TraceHilbertSpace
Used by in this Project
separableCounterexampleRepresentation, separableSpace_separableCounterexampleHilbertSpace
completedRootPureState
MathlibAnnex.CStarAlgebra.CAR.completedRootPureState
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
isPureState_rootState
Used by in this Project
exists_selectedCyclicUnitary, representativeShellData_root_alpha, representativeShellData_root_link
isStarProjection_transportedFlag
MathlibAnnex.CStarAlgebra.CAR.isStarProjection_transportedFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_rootFlag, transportedFlag
Used by in this Project
exists_targetShellReconstruction, initialFixedProjection_eq_zero_on_otherCyclic, initialFixedProjection_maps_ownCyclic
liftedCornerExponential_commute_stage
MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponential_commute_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
liftedCornerExponential, ofStage_commute_cornerLift
Used by in this Project
liftedCornerExponentialPath_commute_stage
norm_reconstructedStageVector_eq_one
MathlibAnnex.CStarAlgebra.CAR.norm_reconstructedStageVector_eq_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
reconstructedStageVector_vectorFunctional_eq_on_stage
Used by in this Project
exists_unitVector_vectorFunctional_eq_on_stage
norm_rootRepresentation_le
MathlibAnnex.CStarAlgebra.CAR.norm_rootRepresentation_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
norm_leftMulMapPreGNS_apply_le
Used by in this Project
rootRepresentationCLM
representativeLink_initial
MathlibAnnex.CStarAlgebra.CAR.representativeLink_initial
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootShell, transportedFlag
Used by in this Project
exists_completedAtomicShellModel, exists_targetShellReconstruction, trace_transportedFlag_eq_trace_rootFlag
rootGNSNontrivial
MathlibAnnex.CStarAlgebra.CAR.rootGNSNontrivial
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootPositiveState_one
Used by in this Project
rootRepresentation_stage_injective
rowAverage
MathlibAnnex.CStarAlgebra.CAR.rowAverage
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
norm_rowAverageLinear_le
Used by in this Project
liftedCornerExponentialPath
tendsto_norm_transported_compressionError
MathlibAnnex.CStarAlgebra.CAR.tendsto_norm_transported_compressionError
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
tendsto_norm_compressionError
Used by in this Project
tendsto_transported_compressionError
traceRepresentation
MathlibAnnex.CStarAlgebra.CAR.traceRepresentation
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
TraceHilbertSpace
Used by in this Project
denseRange_traceRepresentation_orbit, inner_traceVector_traceRepresentation
traceVector
MathlibAnnex.CStarAlgebra.CAR.traceVector
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
TraceHilbertSpace
Used by in this Project
denseRange_traceRepresentation_orbit, inner_traceVector_traceRepresentation, norm_traceVector
transportedFlag_mul_of_le
MathlibAnnex.CStarAlgebra.CAR.transportedFlag_mul_of_le
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootFlag_mul_of_le, transportedFlag
Used by in this Project
exists_completedAtomicShellModel, exists_targetShellReconstruction
transportedFlag_zero
MathlibAnnex.CStarAlgebra.CAR.transportedFlag_zero
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootFlag_zero, transportedFlag
Used by in this Project
exists_completedAtomicShellModel, exists_targetShellReconstruction, trace_transportedFlag_eq_trace_rootFlag
Level 35
14 declarationsdenseRange_traceRepresentation_orbit
MathlibAnnex.CStarAlgebra.CAR.denseRange_traceRepresentation_orbit
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
traceRepresentation, traceVector
Used by in this Project
exists_linearIsometryEquiv_traceHilbertSpace, separableSpace_traceHilbertSpace
exists_selectedCyclicUnitary
MathlibAnnex.CStarAlgebra.CAR.exists_selectedCyclicUnitary
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
completedRootPureState, selected_vectorFunctional
Used by in this Project
isOrtho_cyclicSubspace_of_selectedStates
inner_traceVector_traceRepresentation
MathlibAnnex.CStarAlgebra.CAR.inner_traceVector_traceRepresentation
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
traceRepresentation, traceVector
Used by in this Project
exists_linearIsometryEquiv_traceHilbertSpace
liftedCornerExponentialPath
MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponentialPath
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
liftedCornerExponential, preNormedAlgebra, rowAverage
Used by in this Project
liftedCornerExponentialPairPath, liftedCornerExponentialPath_commute_stage
norm_traceVector
MathlibAnnex.CStarAlgebra.CAR.norm_traceVector
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
tracePositive_one, traceVector
Used by in this Project
traceVector_ne_zero
representativeShellData_root_alpha
MathlibAnnex.CStarAlgebra.CAR.representativeShellData_root_alpha
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
completedRootPureState, representativeShellData
Used by in this Project
transportedFlag_root
representativeShellData_root_link
MathlibAnnex.CStarAlgebra.CAR.representativeShellData_root_link
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
completedRootPureState, representativeShellData, rootShell
Used by in this Project
exists_completedAtomicShellModel
rootRepresentationCLM
MathlibAnnex.CStarAlgebra.CAR.rootRepresentationCLM
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
norm_rootRepresentation_le
Used by in this Project
norm_rootRepresentation
rootRepresentation_stage_injective
MathlibAnnex.CStarAlgebra.CAR.rootRepresentation_stage_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootGNSNontrivial, stageIsSimpleRing
Used by in this Project
norm_rootRepresentation_stage
rootShell_identity_family
MathlibAnnex.CStarAlgebra.CAR.rootShell_identity_family
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
completedRootPureState, rootShell_mul_star_rootShell, star_rootShell_mul_rootShell
Used by in this Project
representativeShellDataOfHomogeneity
selectedAtomicRepresentation
MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
completedRootPureState, SelectedAtomicHilbert, selectedRepresentation
Used by in this Project
AtomicTarget, exists_selectedAtomicCyclicIsometry, representedInitialFlag
selectedVector_fixed_transportedFlag
MathlibAnnex.CStarAlgebra.CAR.selectedVector_fixed_transportedFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
completedRootPureState, isStarProjection_transportedFlag, rootState_rootFlagShow 2 more
Used by in this Project
exists_nonzero_targetFixedSpace, selected_commonFixedProjection_eq_rankOne
tendsto_transported_compressionError
MathlibAnnex.CStarAlgebra.CAR.tendsto_transported_compressionError
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
tendsto_norm_transported_compressionError
Used by in this Project
tendsto_representative_transported_compression
trace_transportedFlag_eq_trace_rootFlag
MathlibAnnex.CStarAlgebra.CAR.trace_transportedFlag_eq_trace_rootFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
representativeLink_final, representativeLink_initial, trace_mul_commShow 1 more
Used by in this Project
trace_transportedFlag
Level 36
13 declarationsAtomicTarget
MathlibAnnex.CStarAlgebra.CAR.AtomicTarget
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
concreteTarget, selectedAtomicRepresentation
Used by in this Project
ShellFamilyTarget, representedGeneratorUnitary, restrictedRepresentation
isOrtho_cyclicSubspace_of_selectedStates
MathlibAnnex.CStarAlgebra.CAR.isOrtho_cyclicSubspace_of_selectedStates
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_selectedCyclicUnitary, no_unitaryIntertwiner_selectedRepresentation
Used by in this Project
initialFixedProjection_eq_zero_on_otherCyclic
liftedCornerExponentialPairPath
MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponentialPairPath
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
liftedCornerExponentialPath
Used by in this Project
liftedCornerExponentialPairPath_commute_stage
liftedCornerExponentialPath_commute_stage
MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponentialPath_commute_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
liftedCornerExponentialPath, liftedCornerExponential_commute_stage
Used by in this Project
liftedCornerExponentialPairPath_commute_stage
norm_rootRepresentation_stage
MathlibAnnex.CStarAlgebra.CAR.norm_rootRepresentation_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
norm_ofStage, rootRepresentation_stage_injective
Used by in this Project
norm_rootRepresentation
representedInitialFlag
MathlibAnnex.CStarAlgebra.CAR.representedInitialFlag
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
selectedAtomicRepresentation, transportedFlag
Used by in this Project
instHasOrthogonalProjectionIInfRepresentedInitialFlag, instHasOrthogonalProjectionRepresentedInitialFlag
representedRootFlag
MathlibAnnex.CStarAlgebra.CAR.representedRootFlag
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
rootFlag, selectedAtomicRepresentation
Used by in this Project
instHasOrthogonalProjectionRepresentedRootFlag, representedFinalFlag
representedShellLink
MathlibAnnex.CStarAlgebra.CAR.representedShellLink
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
representativeShellData, selectedAtomicRepresentation
Used by in this Project
exists_completedAtomicShellModel, representedGenerator_comp_sourceShell
separableSpace_traceHilbertSpace
MathlibAnnex.CStarAlgebra.CAR.separableSpace_traceHilbertSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
denseRange_traceRepresentation_orbit, limitSeparableSpace
Used by in this Project
separableSpace_separableCounterexampleHilbertSpace
tendsto_representative_transported_compression
MathlibAnnex.CStarAlgebra.CAR.tendsto_representative_transported_compression
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
completedRootPureState, tendsto_transported_compressionError, transportedFlag
Used by in this Project
exists_targetDefectVectors_of_fixedSpace_ne_bot, initialFixedProjection_eq_zero_on_otherCyclic, initialFixedProjection_maps_ownCyclic
traceVector_ne_zero
MathlibAnnex.CStarAlgebra.CAR.traceVector_ne_zero
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
norm_traceVector
Used by in this Project
nontrivial_traceHilbertSpace
trace_transportedFlag
MathlibAnnex.CStarAlgebra.CAR.trace_transportedFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
trace_rootFlag, trace_transportedFlag_eq_trace_rootFlag
Used by in this Project
tendsto_transportedFlag_orbit_zero
transportedFlag_root
MathlibAnnex.CStarAlgebra.CAR.transportedFlag_root
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
representativeShellData_root_alpha, transportedFlag
Used by in this Project
exists_surjective_selectedAtomicCyclicIsometry, instHasOrthogonalProjectionIInfRepresentedFinalFlag
Level 37
14 declarationsinitialFixedProjection_eq_zero_on_otherCyclic
MathlibAnnex.CStarAlgebra.CAR.initialFixedProjection_eq_zero_on_otherCyclic
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isOrtho_cyclicSubspace_of_selectedStates, isStarProjection_transportedFlag, tendsto_representative_transported_compression
Used by in this Project
exists_selectedAtomicCyclicIsometry
initialFixedProjection_maps_ownCyclic
MathlibAnnex.CStarAlgebra.CAR.initialFixedProjection_maps_ownCyclic
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_transportedFlag, tendsto_representative_transported_compression
Used by in this Project
exists_selectedAtomicCyclicIsometry
instHasOrthogonalProjectionRepresentedInitialFlag
MathlibAnnex.CStarAlgebra.CAR.instHasOrthogonalProjectionRepresentedInitialFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_transportedFlag, representedInitialFlag
Used by in this Project
selectedAtomicRepresentation_transportedFlag_eq_starProjection
instHasOrthogonalProjectionRepresentedRootFlag
MathlibAnnex.CStarAlgebra.CAR.instHasOrthogonalProjectionRepresentedRootFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_rootFlag, representedRootFlag
Used by in this Project
instHasOrthogonalProjectionRepresentedFinalFlag, selectedAtomicRepresentation_rootFlag_eq_starProjection
liftedCornerExponentialPairPath_commute_stage
MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponentialPairPath_commute_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
liftedCornerExponentialPairPath, liftedCornerExponentialPath_commute_stage
Used by in this Project
exists_delta_liftedCornerUnitary_path_apply_sub_norm_lt
nontrivial_traceHilbertSpace
MathlibAnnex.CStarAlgebra.CAR.nontrivial_traceHilbertSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
traceVector_ne_zero
Used by in this Project
atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation
norm_rootRepresentation
MathlibAnnex.CStarAlgebra.CAR.norm_rootRepresentation
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
dense_stageRange, norm_rootRepresentation_stage, rootRepresentationCLM
Used by in this Project
rootRepresentation_injective
representedFinalFlag
MathlibAnnex.CStarAlgebra.CAR.representedFinalFlag
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
RepresentativeShellFamily, representedRootFlag
Used by in this Project
instHasOrthogonalProjectionIInfRepresentedFinalFlag, instHasOrthogonalProjectionRepresentedFinalFlag
representedGeneratorUnitary
MathlibAnnex.CStarAlgebra.CAR.representedGeneratorUnitary
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
generator, AtomicTarget
Used by in this Project
representedGenerator_comp_sourceShell
restrictedRepresentation
MathlibAnnex.CStarAlgebra.CAR.restrictedRepresentation
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
sourceHom, AtomicTarget
Used by in this Project
representedGenerator_comp_sourceShell
selected_commonFixedProjection_eq_rankOne
MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_rankOne
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
selectedVector_fixed_transportedFlag, tendsto_representative_transported_compression
Used by in this Project
iInf_range_atomic_transportedFlag_eq_span
selected_commonFixedProjection_eq_zero
MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_zero
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_transportedFlag, tendsto_representative_transported_compression, instNontrivial
Used by in this Project
iInf_range_atomic_transportedFlag_eq_span
separableSpace_separableCounterexampleHilbertSpace
MathlibAnnex.CStarAlgebra.CAR.separableSpace_separableCounterexampleHilbertSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
SeparableCounterexampleHilbertSpace, separableSpace_traceHilbertSpace
Used by in this Project
atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation, cardinalMk_atomicCounterexampleAlgebra_le_continuum
tendsto_transportedFlag_orbit_zero
MathlibAnnex.CStarAlgebra.CAR.tendsto_transportedFlag_orbit_zero
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_transportedFlag, tracePositive, trace_transportedFlag
Used by in this Project
exists_shell_sums_eq_on_cyclicSubspace
Level 38
7 declarationsexists_selectedAtomicCyclicIsometry
MathlibAnnex.CStarAlgebra.CAR.exists_selectedAtomicCyclicIsometry
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
initialFixedProjection_eq_zero_on_otherCyclic, initialFixedProjection_maps_ownCyclic, rootState_rootFlagShow 2 more
Used by in this Project
exists_surjective_selectedAtomicCyclicIsometry
iInf_range_atomic_transportedFlag_eq_span
MathlibAnnex.CStarAlgebra.CAR.iInf_range_atomic_transportedFlag_eq_span
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
selected_commonFixedProjection_eq_rankOne, selected_commonFixedProjection_eq_zero, selectedEmbedding
Used by in this Project
ambientInclusion_unitaryEquivalent, instHasOrthogonalProjectionIInfRepresentedFinalFlag, instHasOrthogonalProjectionIInfRepresentedInitialFlag
instHasOrthogonalProjectionRepresentedFinalFlag
MathlibAnnex.CStarAlgebra.CAR.instHasOrthogonalProjectionRepresentedFinalFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
instHasOrthogonalProjectionRepresentedRootFlag, representedFinalFlag
Used by in this Project
exists_completedAtomicShellModel
representedGenerator_comp_sourceShell
MathlibAnnex.CStarAlgebra.CAR.representedGenerator_comp_sourceShell
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
representedGeneratorUnitary, representedShellLink, restrictedRepresentationShow 1 more
Used by in this Project
exists_targetShellReconstruction
rootRepresentation_injective
MathlibAnnex.CStarAlgebra.CAR.rootRepresentation_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
norm_rootRepresentation
Used by in this Project
exists_rootState_mul_ne_zero
selectedAtomicRepresentation_rootFlag_eq_starProjection
MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation_rootFlag_eq_starProjection
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
instHasOrthogonalProjectionRepresentedRootFlag
Used by in this Project
exists_completedAtomicShellModel
selectedAtomicRepresentation_transportedFlag_eq_starProjection
MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation_transportedFlag_eq_starProjection
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
instHasOrthogonalProjectionRepresentedInitialFlag
Used by in this Project
exists_completedAtomicShellModel
Level 39
4 declarationsexists_rootState_mul_ne_zero
MathlibAnnex.CStarAlgebra.CAR.exists_rootState_mul_ne_zero
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
rootRepresentation_injective
Used by in this Project
exists_rootFlag_mem_of_ne_zero_mem
exists_targetShellReconstruction
MathlibAnnex.CStarAlgebra.CAR.exists_targetShellReconstruction
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_transportedFlag, representativeLink_final, representativeLink_initial
Used by in this Project
exists_shell_sums_eq_on_cyclicSubspace, exists_targetDefectVectors_of_fixedSpace_ne_bot, isIrreducible_restrictedRepresentation_of_all_fixed_bot
instHasOrthogonalProjectionIInfRepresentedFinalFlag
MathlibAnnex.CStarAlgebra.CAR.instHasOrthogonalProjectionIInfRepresentedFinalFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
iInf_range_atomic_transportedFlag_eq_span, representedFinalFlag, transportedFlag_root
Used by in this Project
exists_completedAtomicShellModel
instHasOrthogonalProjectionIInfRepresentedInitialFlag
MathlibAnnex.CStarAlgebra.CAR.instHasOrthogonalProjectionIInfRepresentedInitialFlag
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
iInf_range_atomic_transportedFlag_eq_span, representedInitialFlag
Used by in this Project
exists_completedAtomicShellModel
Level 40
3 declarationsexists_rootFlag_mem_of_ne_zero_mem
MathlibAnnex.CStarAlgebra.CAR.exists_rootFlag_mem_of_ne_zero_mem
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_rootState_mul_ne_zero, tendsto_norm_compressionError
Used by in this Project
limitIsSimpleRing
exists_targetDefectVectors_of_fixedSpace_ne_bot
MathlibAnnex.CStarAlgebra.CAR.exists_targetDefectVectors_of_fixedSpace_ne_bot
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_targetShellReconstruction, tendsto_representative_transported_compression
Used by in this Project
exists_targetDefectVectors
isIrreducible_restrictedRepresentation_of_all_fixed_bot
MathlibAnnex.CStarAlgebra.CAR.isIrreducible_restrictedRepresentation_of_all_fixed_bot
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
reduces_concreteTarget_of_generators, exists_targetShellReconstruction
Used by in this Project
exists_nonzero_targetFixedSpace
Level 41
2 declarationsexists_nonzero_targetFixedSpace
MathlibAnnex.CStarAlgebra.CAR.exists_nonzero_targetFixedSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isIrreducible_restrictedRepresentation_of_all_fixed_bot, selectedVector_fixed_transportedFlag, positiveLinearMapOfMemStateSpace
Used by in this Project
exists_targetDefectVectors
limitIsSimpleRing
MathlibAnnex.CStarAlgebra.CAR.limitIsSimpleRing
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_rootFlag_mem_of_ne_zero_mem, limitNontrivial
Used by in this Project
isSimpleCStarAlgebra_limit, representation_injective, selectedRootRepresentation_injective
Level 42
4 declarationsexists_targetDefectVectors
MathlibAnnex.CStarAlgebra.CAR.exists_targetDefectVectors
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_nonzero_targetFixedSpace, exists_targetDefectVectors_of_fixedSpace_ne_bot
Used by in this Project
exists_targetDefectVectorFamily
isSimpleCStarAlgebra_limit
MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_limit
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitIsSimpleRing, IsSimpleCStarAlgebra
Used by in this Project
eq_zero_of_isCompactOperator_image
representation_injective
MathlibAnnex.CStarAlgebra.CAR.representation_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
limitIsSimpleRing
Used by in this Project
eq_zero_of_isCompactOperator_image
selectedRootRepresentation_injective
MathlibAnnex.CStarAlgebra.CAR.selectedRootRepresentation_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
completedRootPureState, limitIsSimpleRing, instNontrivialShow 1 more
Used by in this Project
selectedAtomicRepresentation_injective
Level 43
3 declarationseq_zero_of_isCompactOperator_image
MathlibAnnex.CStarAlgebra.CAR.eq_zero_of_isCompactOperator_image
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isSimpleCStarAlgebra_limit, not_finiteDimensional, representation_injective
Used by in this Project
not_finiteDimensional_range_rootCorner
exists_targetDefectVectorFamily
MathlibAnnex.CStarAlgebra.CAR.exists_targetDefectVectorFamily
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_targetDefectVectors
Used by in this Project
exists_surjective_selectedAtomicCyclicIsometry
selectedAtomicRepresentation_injective
MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
selectedAtomicRepresentation, selectedRootRepresentation_injective
Used by in this Project
exists_completedAtomicShellModel
Level 44
3 declarationsexists_completedAtomicShellModel
MathlibAnnex.CStarAlgebra.CAR.exists_completedAtomicShellModel
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_irreducible_pureAtomicShellModel, sourceHom_injective, instHasOrthogonalProjectionIInfRepresentedFinalFlagShow 11 more
Used by in this Project
shellFamilyLinks
exists_surjective_selectedAtomicCyclicIsometry
MathlibAnnex.CStarAlgebra.CAR.exists_surjective_selectedAtomicCyclicIsometry
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_selectedAtomicCyclicIsometry, exists_targetDefectVectorFamily, transportedFlag_root
Used by in this Project
ambientInclusion_unitaryEquivalent
not_finiteDimensional_range_rootCorner
MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional_range_rootCorner
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
eq_zero_of_isCompactOperator_image, limitMatrixUnit, matrixUnit_apply
Used by in this Project
exists_rootCornerFamily_with_gram, exists_rootCornerSupported_exponential_apply_eq_involution
Level 45
4 declarationsambientInclusion_unitaryEquivalent
MathlibAnnex.CStarAlgebra.CAR.ambientInclusion_unitaryEquivalent
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
intertwines_concreteTarget_of_generators, exists_surjective_selectedAtomicCyclicIsometry, iInf_range_atomic_transportedFlag_eq_span
Used by in this Project
isUniqueIrreducibleModel_shellFamilyInclusion
exists_rootCornerFamily_with_gram
MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerFamily_with_gram
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isStarProjection_limitMatrixUnit_zero_zero, not_finiteDimensional_range_rootCorner
Used by in this Project
exists_unitVector_vectorFunctional_eq_on_stage
exists_rootCornerSupported_exponential_apply_eq_involution
MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerSupported_exponential_apply_eq_involution
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_rootCornerSupported_exponential_eq_on, not_finiteDimensional_range_rootCorner, rootCornerSubspace
Used by in this Project
exists_liftedCornerExponential_apply_eq_involution
shellFamilyLinks
MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
exists_completedAtomicShellModel
Used by in this Project
ShellFamilyTarget, shellFamilyLinks_map_selectedVector, shellFamilyLinks_rootShow 2 more
Level 46
7 declarationsShellFamilyTarget
MathlibAnnex.CStarAlgebra.CAR.ShellFamilyTarget
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
AtomicTarget, shellFamilyLinks
Used by in this Project
AtomicCounterexampleAlgebra, isClosed_shellFamilyTarget, shellFamilyGenerator
exists_liftedCornerExponential_apply_eq_involution
MathlibAnnex.CStarAlgebra.CAR.exists_liftedCornerExponential_apply_eq_involution
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_rootCornerSupported_exponential_apply_eq_involution, representation_liftedCornerExponential_apply_of_root
Used by in this Project
exists_delta_liftedCornerUnitary_path_apply_sub_norm_lt
exists_unitVector_vectorFunctional_eq_on_stage
MathlibAnnex.CStarAlgebra.CAR.exists_unitVector_vectorFunctional_eq_on_stage
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_rootCornerFamily_with_gram, norm_reconstructedStageVector_eq_one
Used by in this Project
exists_stageTests_crossRepresentation_path_approx, exists_unitary_crossRepresentation_path_approx
shellFamilyLinks_map_selectedVector
MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks_map_selectedVector
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
shellFamilyLinks
Used by in this Project
isUniqueIrreducibleModel_shellFamilyInclusion
shellFamilyLinks_root
MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks_root
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
shellFamilyLinks
Used by in this Project
isUniqueIrreducibleModel_shellFamilyInclusion
shellFamilyLinks_sourceShell
MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks_sourceShell
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
shellFamilyLinks
Used by in this Project
exists_shell_sums_eq_on_cyclicSubspace, isUniqueIrreducibleModel_shellFamilyInclusion
shellFamilyLinks_unitary
MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks_unitary
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
shellFamilyLinks
Used by in this Project
exists_shell_sums_eq_on_cyclicSubspace, isUniqueIrreducibleModel_shellFamilyInclusion
Level 47
6 declarationsexists_delta_liftedCornerUnitary_path_apply_sub_norm_lt
MathlibAnnex.CStarAlgebra.CAR.exists_delta_liftedCornerUnitary_path_apply_sub_norm_lt
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_liftedCornerExponential_apply_eq_involution, liftedCornerExponentialPairPath_commute_stage
Used by in this Project
exists_delta_stageCentral_unitary_path_apply_sub_norm_lt
isClosed_shellFamilyTarget
MathlibAnnex.CStarAlgebra.CAR.isClosed_shellFamilyTarget
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ShellFamilyTarget
Used by in this Project
shellFamilyEndpoint
shellFamilyGenerator
MathlibAnnex.CStarAlgebra.CAR.shellFamilyGenerator
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
ShellFamilyTarget
Used by in this Project
exists_shell_sums_eq_on_cyclicSubspace
shellFamilyInclusion
MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
ShellFamilyTarget
Used by in this Project
atomicCounterexampleRepresentation, isIrreducible_shellFamilyInclusion, shellFamilyInclusion_injective
shellFamilySourceHom
MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
ShellFamilyTarget
Used by in this Project
apply_shellFamilySourceHom_eq_trace_of_apply_one_of_mul_comm, exists_shell_sums_eq_on_cyclicSubspace, shellFamilySourceHom_injectiveShow 1 more
shellFamilyTargetPartialOrder
MathlibAnnex.CStarAlgebra.CAR.shellFamilyTargetPartialOrder
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
ShellFamilyTarget
Used by in this Project
shellFamilyTargetStarOrderedRing
Level 48
7 declarationsexists_delta_stageCentral_unitary_path_apply_sub_norm_lt
MathlibAnnex.CStarAlgebra.CAR.exists_delta_stageCentral_unitary_path_apply_sub_norm_lt
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_delta_liftedCornerUnitary_path_apply_sub_norm_lt, sum_norm_sq_map_limitMatrixUnit_star
Used by in this Project
exists_delta_exact_unitary_path_apply_eq_and_stage_commutator
exists_shell_sums_eq_on_cyclicSubspace
MathlibAnnex.CStarAlgebra.CAR.exists_shell_sums_eq_on_cyclicSubspace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_targetShellReconstruction, shellFamilyGenerator, shellFamilyLinks_sourceShell
Used by in this Project
reduces_cyclicSubspace_of_trace
isIrreducible_shellFamilyInclusion
MathlibAnnex.CStarAlgebra.CAR.isIrreducible_shellFamilyInclusion
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
shellFamilyInclusion
Used by in this Project
isUniqueIrreducibleModel_shellFamilyInclusion
shellFamilyInclusion_injective
MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ambientInclusion_injective, shellFamilyInclusion
Used by in this Project
isUniqueIrreducibleModel_shellFamilyInclusion
shellFamilySourceHom_injective
MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
shellFamilySourceHom
Used by in this Project
exists_state_extension_trace, not_finiteDimensional_shellFamilyTarget, shellFamilyTargetNontrivial
shellFamilySourceHom_map_one
MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom_map_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
shellFamilySourceHom
Used by in this Project
shellFamilyEndpoint
shellFamilyTargetStarOrderedRing
MathlibAnnex.CStarAlgebra.CAR.shellFamilyTargetStarOrderedRing
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
shellFamilyTargetPartialOrder
Used by in this Project
apply_shellFamilySourceHom_eq_trace_of_apply_one_of_mul_comm, exists_state_extension_trace, isSimpleCStarAlgebra_shellFamilyTargetShow 1 more
Level 49
7 declarationsapply_shellFamilySourceHom_eq_trace_of_apply_one_of_mul_comm
MathlibAnnex.CStarAlgebra.CAR.apply_shellFamilySourceHom_eq_trace_of_apply_one_of_mul_comm
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
eq_trace_of_apply_one_of_mul_comm, shellFamilySourceHom, shellFamilyTargetStarOrderedRing
Used by in this Project
eq_traceExtension_of_mem_stateSpace_of_mul_comm
exists_delta_exact_unitary_path_apply_eq_and_stage_commutator
MathlibAnnex.CStarAlgebra.CAR.exists_delta_exact_unitary_path_apply_eq_and_stage_commutator
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_delta_stageCentral_unitary_path_apply_sub_norm_lt
Used by in this Project
exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt, exists_unitary_crossRepresentation_path_approx
exists_state_extension_trace
MathlibAnnex.CStarAlgebra.CAR.exists_state_extension_trace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
norm_trace_le, shellFamilySourceHom_injective, shellFamilyTargetStarOrderedRingShow 1 more
Used by in this Project
traceExtension
isUniqueIrreducibleModel_shellFamilyInclusion
MathlibAnnex.CStarAlgebra.CAR.isUniqueIrreducibleModel_shellFamilyInclusion
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ambientInclusion_unitaryEquivalent, isIrreducible_shellFamilyInclusion, shellFamilyInclusion_injective
Used by in this Project
continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra, isSimpleCStarAlgebra_shellFamilyTarget, isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion
not_finiteDimensional_shellFamilyTarget
MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional_shellFamilyTarget
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
not_finiteDimensional, shellFamilySourceHom_injective, shellFamilyTargetStarOrderedRing
Used by in this Project
continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra, not_isCompactOperatorModel_shellFamilyTarget
reduces_cyclicSubspace_of_trace
MathlibAnnex.CStarAlgebra.CAR.reduces_cyclicSubspace_of_trace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
reduces_concreteTarget_of_generators, exists_shell_sums_eq_on_cyclicSubspace
Used by in this Project
cyclicSubspace_eq_top_of_trace_of_cyclic
shellFamilyTargetNontrivial
MathlibAnnex.CStarAlgebra.CAR.shellFamilyTargetNontrivial
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
shellFamilySourceHom_injective
Used by in this Project
continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra, isSimpleCStarAlgebra_shellFamilyTarget, nontrivial_shellFamilyTargetShow 1 more
Level 50
8 declarationscyclicSubspace_eq_top_of_trace_of_cyclic
MathlibAnnex.CStarAlgebra.CAR.cyclicSubspace_eq_top_of_trace_of_cyclic
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
reduces_cyclicSubspace_of_trace
Used by in this Project
denseRange_source_orbit_of_trace_of_cyclic, stronglyConverges_shell_sums_of_trace_of_cyclic
exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt
MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_common_stage_approx, exists_delta_exact_unitary_path_apply_eq_and_stage_commutator
Used by in this Project
exists_stageTests_crossRepresentation_path_approx
exists_unitary_crossRepresentation_path_approx
MathlibAnnex.CStarAlgebra.CAR.exists_unitary_crossRepresentation_path_approx
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_common_stage_approx, exists_delta_exact_unitary_path_apply_eq_and_stage_commutator, exists_unitVector_vectorFunctional_eq_on_stage
Used by in this Project
nonempty_initialState
isSimpleCStarAlgebra_shellFamilyTarget
MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_shellFamilyTarget
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isUniqueIrreducibleModel_shellFamilyInclusion, shellFamilyTargetNontrivial, shellFamilyTargetStarOrderedRing
Used by in this Project
shellFamilyTarget_closedIdeal_dichotomy
isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion
MathlibAnnex.CStarAlgebra.CAR.isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isUniqueIrreducibleModel_shellFamilyInclusion
Used by in this Project
existsNaimarkCounterexampleOfDensity_continuum, shellFamilyInclusion_unitaryEquivalent_nonUnital
nontrivial_shellFamilyTarget
MathlibAnnex.CStarAlgebra.CAR.nontrivial_shellFamilyTarget
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
shellFamilyTargetNontrivial
Used by in this Project
shellFamilyEndpoint
not_isCompactOperatorModel_shellFamilyTarget
MathlibAnnex.CStarAlgebra.CAR.not_isCompactOperatorModel_shellFamilyTarget
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
not_finiteDimensional_shellFamilyTarget, shellFamilyTargetNontrivial
Used by in this Project
existsNaimarkCounterexampleOfDensity_continuum, shellFamilyTarget_not_compactOperatorModel
traceExtension
MathlibAnnex.CStarAlgebra.CAR.traceExtension
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
exists_state_extension_trace
Used by in this Project
traceExtension_mem_stateSpace, traceExtension_shellFamilySourceHom
Level 51
8 declarationsdenseRange_source_orbit_of_trace_of_cyclic
MathlibAnnex.CStarAlgebra.CAR.denseRange_source_orbit_of_trace_of_cyclic
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
cyclicSubspace_eq_top_of_trace_of_cyclic
Used by in this Project
denseRange_tracialRepresentation_source_orbit, exists_pointed_unitary_of_trace_of_cyclic
exists_stageTests_crossRepresentation_path_approx
MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_crossRepresentation_path_approx
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt, exists_unitVector_vectorFunctional_eq_on_stage
Used by in this Project
nonempty_initialState, nonempty_transition
shellFamilyInclusion_unitaryEquivalent_nonUnital
MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion_unitaryEquivalent_nonUnital
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion
Used by in this Project
shellFamily_captures_nonunital
shellFamilyTarget_closedIdeal_dichotomy
MathlibAnnex.CStarAlgebra.CAR.shellFamilyTarget_closedIdeal_dichotomy
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
isSimpleCStarAlgebra_shellFamilyTarget
Used by in this Project
shellFamilyEndpoint, tracialRepresentation_injective
shellFamilyTarget_not_compactOperatorModel
MathlibAnnex.CStarAlgebra.CAR.shellFamilyTarget_not_compactOperatorModel
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
not_isCompactOperatorModel_shellFamilyTarget
Used by in this Project
shellFamilyEndpoint
stronglyConverges_shell_sums_of_trace_of_cyclic
MathlibAnnex.CStarAlgebra.CAR.stronglyConverges_shell_sums_of_trace_of_cyclic
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
cyclicSubspace_eq_top_of_trace_of_cyclic
Used by in this Project
exists_pointed_unitary_of_trace_of_cyclic
traceExtension_mem_stateSpace
MathlibAnnex.CStarAlgebra.CAR.traceExtension_mem_stateSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
traceExtension
Used by in this Project
traceExtensionPositive
traceExtension_shellFamilySourceHom
MathlibAnnex.CStarAlgebra.CAR.traceExtension_shellFamilySourceHom
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
traceExtension
Used by in this Project
vectorFunctional_tracialRepresentation_source
Level 52
5 declarationsexists_pointed_unitary_of_trace_of_cyclic
MathlibAnnex.CStarAlgebra.CAR.exists_pointed_unitary_of_trace_of_cyclic
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
intertwines_of_source_of_generators, denseRange_source_orbit_of_trace_of_cyclic, stronglyConverges_shell_sums_of_trace_of_cyclic
Used by in this Project
eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace
nonempty_initialState
MathlibAnnex.CStarAlgebra.CAR.nonempty_initialState
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
AlternatingState, exists_stageTests_crossRepresentation_path_approx, exists_unitary_crossRepresentation_path_approxShow 3 more
Used by in this Project
initialState
nonempty_transition
MathlibAnnex.CStarAlgebra.CAR.nonempty_transition
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
AlternatingTransition, exists_stageTests_crossRepresentation_path_approx, mem_densePrefixShow 3 more
Used by in this Project
chosenTransition
shellFamily_captures_nonunital
MathlibAnnex.CStarAlgebra.CAR.shellFamily_captures_nonunital
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
shellFamilyInclusion_unitaryEquivalent_nonUnital
Used by in this Project
shellFamilyEndpoint
traceExtensionPositive
MathlibAnnex.CStarAlgebra.CAR.traceExtensionPositive
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
traceExtension_mem_stateSpace, positiveLinearMapOfMemStateSpace
Used by in this Project
TracialHilbertSpace, traceExtensionPositive_one
Level 53
5 declarationsTracialHilbertSpace
MathlibAnnex.CStarAlgebra.CAR.TracialHilbertSpace
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
traceExtensionPositive
Used by in this Project
tracialRepresentation, tracialVector
chosenTransition
MathlibAnnex.CStarAlgebra.CAR.chosenTransition
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
nonempty_transition
Used by in this Project
alternatingStates
initialState
MathlibAnnex.CStarAlgebra.CAR.initialState
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
nonempty_initialState
Used by in this Project
alternatingStates
shellFamilyEndpoint
MathlibAnnex.CStarAlgebra.CAR.shellFamilyEndpoint
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
ShellFamilyEndpoint, isClosed_shellFamilyTarget, nontrivial_shellFamilyTarget
Used by in this Project
atomicCounterexampleEndpoint
traceExtensionPositive_one
MathlibAnnex.CStarAlgebra.CAR.traceExtensionPositive_one
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
traceExtensionPositive
Used by in this Project
norm_tracialVector
Level 54
3 declarationsalternatingStates
MathlibAnnex.CStarAlgebra.CAR.alternatingStates
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
chosenTransition, initialState
Used by in this Project
alternatingTransitions, leftAutomorphisms, outputUnitaryShow 1 more
tracialRepresentation
MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
TracialHilbertSpace
Used by in this Project
denseRange_tracialRepresentation_orbit, inner_tracialVector_tracialRepresentation, tracialRepresentation_injective
tracialVector
MathlibAnnex.CStarAlgebra.CAR.tracialVector
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
TracialHilbertSpace
Used by in this Project
denseRange_tracialRepresentation_orbit, inner_tracialVector_tracialRepresentation, norm_tracialVector
Level 55
7 declarationsalternatingTransitions
MathlibAnnex.CStarAlgebra.CAR.alternatingTransitions
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
alternatingStates
Used by in this Project
leftAutomorphisms_step, leftAutomorphisms_symm_step, outputAutomorphisms_state_denseShow 2 more
denseRange_tracialRepresentation_orbit
MathlibAnnex.CStarAlgebra.CAR.denseRange_tracialRepresentation_orbit
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
tracialRepresentation, tracialVector
Used by in this Project
denseRange_tracialRepresentation_source_orbit, eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace
inner_tracialVector_tracialRepresentation
MathlibAnnex.CStarAlgebra.CAR.inner_tracialVector_tracialRepresentation
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
tracialRepresentation, tracialVector
Used by in this Project
vectorFunctional_tracialRepresentation, vectorFunctional_tracialRepresentation_source
leftAutomorphisms
MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
alternatingStates
Used by in this Project
leftAutomorphisms_step, leftAutomorphisms_symm_step, outputAutomorphisms_eq
norm_tracialVector
MathlibAnnex.CStarAlgebra.CAR.norm_tracialVector
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
traceExtensionPositive_one, tracialVector
Used by in this Project
traceExtension_star_unitary_mul_mul, tracialVector_ne_zero
outputUnitary
MathlibAnnex.CStarAlgebra.CAR.outputUnitary
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
alternatingStates
Used by in this Project
outputAutomorphisms
rightAutomorphisms
MathlibAnnex.CStarAlgebra.CAR.rightAutomorphisms
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
alternatingStates
Used by in this Project
outputAutomorphisms_eq, rightAutomorphisms_step, rightAutomorphisms_symm_step
Level 56
8 declarationsleftAutomorphisms_step
MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_step
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
alternatingTransitions, leftAutomorphisms, mem_protectedPrefix
Used by in this Project
leftAutomorphisms_cauchy
leftAutomorphisms_symm_step
MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_symm_step
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
alternatingTransitions, leftAutomorphisms, mem_symm_protectedPrefix
Used by in this Project
leftAutomorphisms_symm_cauchy
outputAutomorphisms
MathlibAnnex.CStarAlgebra.CAR.outputAutomorphisms
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
outputUnitary
Used by in this Project
outputAutomorphisms_eq
rightAutomorphisms_step
MathlibAnnex.CStarAlgebra.CAR.rightAutomorphisms_step
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
alternatingTransitions, mem_protectedPrefix, rightAutomorphisms
Used by in this Project
rightAutomorphisms_cauchy
rightAutomorphisms_symm_step
MathlibAnnex.CStarAlgebra.CAR.rightAutomorphisms_symm_step
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
alternatingTransitions, mem_symm_protectedPrefix, rightAutomorphisms
Used by in this Project
rightAutomorphisms_symm_cauchy
tracialVector_ne_zero
MathlibAnnex.CStarAlgebra.CAR.tracialVector_ne_zero
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
norm_tracialVector
Used by in this Project
nontrivial_tracialHilbertSpace
vectorFunctional_tracialRepresentation
MathlibAnnex.CStarAlgebra.CAR.vectorFunctional_tracialRepresentation
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
inner_tracialVector_tracialRepresentation
Used by in this Project
traceExtension_star_unitary_mul_mul
vectorFunctional_tracialRepresentation_source
MathlibAnnex.CStarAlgebra.CAR.vectorFunctional_tracialRepresentation_source
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
inner_tracialVector_tracialRepresentation, traceExtension_shellFamilySourceHom
Used by in this Project
denseRange_tracialRepresentation_source_orbit, eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace
Level 57
8 declarationsdenseRange_tracialRepresentation_source_orbit
MathlibAnnex.CStarAlgebra.CAR.denseRange_tracialRepresentation_source_orbit
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
denseRange_source_orbit_of_trace_of_cyclic, denseRange_tracialRepresentation_orbit, vectorFunctional_tracialRepresentation_source
Used by in this Project
exists_linearIsometryEquiv_traceHilbertSpace
eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace
MathlibAnnex.CStarAlgebra.CAR.eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
denseRange_tracialRepresentation_orbit, exists_pointed_unitary_of_trace_of_cyclic, vectorFunctional_tracialRepresentation_source
Used by in this Project
eq_traceExtension_of_mem_stateSpace_of_mul_comm, existsUnique_state_extension_trace, traceExtension_star_unitary_mul_mul
leftAutomorphisms_cauchy
MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_cauchy
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
denseRange_transportDense, leftAutomorphisms_step, summable_transportBudget
Used by in this Project
leftAutomorphisms_succ_cauchy
leftAutomorphisms_symm_cauchy
MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_symm_cauchy
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
denseRange_transportDense, leftAutomorphisms_symm_step, summable_transportBudget
Used by in this Project
leftAutomorphisms_succ_symm_cauchy
nontrivial_tracialHilbertSpace
MathlibAnnex.CStarAlgebra.CAR.nontrivial_tracialHilbertSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
tracialVector_ne_zero
Used by in this Project
tracialRepresentation_injective
outputAutomorphisms_eq
MathlibAnnex.CStarAlgebra.CAR.outputAutomorphisms_eq
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
leftAutomorphisms, outputAutomorphisms, rightAutomorphisms
Used by in this Project
outputAutomorphisms_cauchy, outputAutomorphisms_state_dense, outputAutomorphisms_symm_cauchy
rightAutomorphisms_cauchy
MathlibAnnex.CStarAlgebra.CAR.rightAutomorphisms_cauchy
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
denseRange_transportDense, rightAutomorphisms_step, summable_transportBudget
Used by in this Project
outputAutomorphisms_symm_cauchy
rightAutomorphisms_symm_cauchy
MathlibAnnex.CStarAlgebra.CAR.rightAutomorphisms_symm_cauchy
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
denseRange_transportDense, rightAutomorphisms_symm_step, summable_transportBudget
Used by in this Project
outputAutomorphisms_cauchy
Level 58
8 declarationseq_traceExtension_of_mem_stateSpace_of_mul_comm
MathlibAnnex.CStarAlgebra.CAR.eq_traceExtension_of_mem_stateSpace_of_mul_comm
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
apply_shellFamilySourceHom_eq_trace_of_apply_one_of_mul_comm, eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace
Used by in this Project
existsUnique_tracial_state
existsUnique_state_extension_trace
MathlibAnnex.CStarAlgebra.CAR.existsUnique_state_extension_trace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace
Used by in this Project
None in this Project
exists_linearIsometryEquiv_traceHilbertSpace
MathlibAnnex.CStarAlgebra.CAR.exists_linearIsometryEquiv_traceHilbertSpace
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
denseRange_traceRepresentation_orbit, denseRange_tracialRepresentation_source_orbit, inner_traceVector_traceRepresentation
Used by in this Project
traceGNSUnitary
leftAutomorphisms_succ_cauchy
MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_succ_cauchy
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
leftAutomorphisms_cauchy
Used by in this Project
outputAutomorphisms_cauchy
leftAutomorphisms_succ_symm_cauchy
MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_succ_symm_cauchy
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
leftAutomorphisms_symm_cauchy
Used by in this Project
outputAutomorphisms_symm_cauchy
outputAutomorphisms_state_dense
MathlibAnnex.CStarAlgebra.CAR.outputAutomorphisms_state_dense
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
alternatingTransitions, outputAutomorphisms_eq
Used by in this Project
tendsto_outputAutomorphisms_state
traceExtension_star_unitary_mul_mul
MathlibAnnex.CStarAlgebra.CAR.traceExtension_star_unitary_mul_mul
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace, norm_tracialVector, vectorFunctional_tracialRepresentation
Used by in this Project
traceExtension_shellFamilySourceHom_mul
tracialRepresentation_injective
MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
nontrivial_tracialHilbertSpace, shellFamilyTarget_closedIdeal_dichotomy, tracialRepresentation
Used by in this Project
traceModelRepresentation_injective
Level 59
5 declarationsoutputAutomorphisms_cauchy
MathlibAnnex.CStarAlgebra.CAR.outputAutomorphisms_cauchy
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
leftAutomorphisms_succ_cauchy, outputAutomorphisms_eq, rightAutomorphisms_symm_cauchy
Used by in this Project
hasInnerIntertwiningSequence_vectorFunctional
outputAutomorphisms_symm_cauchy
MathlibAnnex.CStarAlgebra.CAR.outputAutomorphisms_symm_cauchy
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
leftAutomorphisms_succ_symm_cauchy, outputAutomorphisms_eq, rightAutomorphisms_cauchy
Used by in this Project
hasInnerIntertwiningSequence_vectorFunctional
tendsto_outputAutomorphisms_state
MathlibAnnex.CStarAlgebra.CAR.tendsto_outputAutomorphisms_state
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
denseRange_transportDense, outputAutomorphisms_state_dense, tendsto_transportBudget_zero
Used by in this Project
hasInnerIntertwiningSequence_vectorFunctional
traceExtension_shellFamilySourceHom_mul
MathlibAnnex.CStarAlgebra.CAR.traceExtension_shellFamilySourceHom_mul
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
traceExtension_star_unitary_mul_mul
Used by in this Project
traceExtension_shellFamilyGenerator_mul
traceGNSUnitary
MathlibAnnex.CStarAlgebra.CAR.traceGNSUnitary
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
exists_linearIsometryEquiv_traceHilbertSpace
Used by in this Project
traceModelRepresentation
Level 60
3 declarationshasInnerIntertwiningSequence_vectorFunctional
MathlibAnnex.CStarAlgebra.CAR.hasInnerIntertwiningSequence_vectorFunctional
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
HasInnerIntertwiningSequence, outputAutomorphisms_cauchy, outputAutomorphisms_symm_cauchyShow 1 more
Used by in this Project
hasInnerIntertwiningSequence_of_pure
traceExtension_shellFamilyGenerator_mul
MathlibAnnex.CStarAlgebra.CAR.traceExtension_shellFamilyGenerator_mul
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
traceExtension_shellFamilySourceHom_mul
Used by in this Project
traceExtension_mul_comm
traceModelRepresentation
MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
traceGNSUnitary
Used by in this Project
separableCounterexampleRepresentation, traceModelRepresentation_injective
Level 61
3 declarationshasInnerIntertwiningSequence_of_pure
MathlibAnnex.CStarAlgebra.CAR.hasInnerIntertwiningSequence_of_pure
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
hasInnerIntertwiningSequence_vectorFunctional, IsPureState, positiveLinearMapOfMemStateSpace_one
Used by in this Project
homogeneity
traceExtension_mul_comm
MathlibAnnex.CStarAlgebra.CAR.traceExtension_mul_comm
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
traceExtension_shellFamilyGenerator_mul
Used by in this Project
existsUnique_tracial_state
traceModelRepresentation_injective
MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
traceModelRepresentation, tracialRepresentation_injective
Used by in this Project
separableCounterexampleRepresentation_injective
Level 62
2 declarationsexistsUnique_tracial_state
MathlibAnnex.CStarAlgebra.CAR.existsUnique_tracial_state
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
eq_traceExtension_of_mem_stateSpace_of_mul_comm, traceExtension_mul_comm
Used by in this Project
None in this Project
homogeneity
MathlibAnnex.CStarAlgebra.CAR.homogeneity
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
hasInnerIntertwiningSequence_of_pure, homogeneity_of_innerIntertwiningSequences
Used by in this Project
representativeShellDataOfHomogeneity
Level 63
1 declarationrepresentativeShellDataOfHomogeneity
MathlibAnnex.CStarAlgebra.CAR.representativeShellDataOfHomogeneity
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
RepresentativeShellData, homogeneity, rootShell_identity_familyShow 1 more
Used by in this Project
representativeShellDataOfHomogeneity_root_alpha, representativeShellDataOfHomogeneity_root_link
Level 64
2 declarationsrepresentativeShellDataOfHomogeneity_root_alpha
MathlibAnnex.CStarAlgebra.CAR.representativeShellDataOfHomogeneity_root_alpha
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
representativeShellDataOfHomogeneity
Used by in this Project
homogeneityShellFamily
representativeShellDataOfHomogeneity_root_link
MathlibAnnex.CStarAlgebra.CAR.representativeShellDataOfHomogeneity_root_link
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
representativeShellDataOfHomogeneity
Used by in this Project
homogeneityShellFamily
Level 65
1 declarationhomogeneityShellFamily
MathlibAnnex.CStarAlgebra.CAR.homogeneityShellFamily
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
RepresentativeShellFamily, representativeShellDataOfHomogeneity_root_alpha, representativeShellDataOfHomogeneity_root_link
Used by in this Project
AtomicCounterexampleAlgebra, AtomicCounterexampleEndpoint
Level 66
2 declarationsAtomicCounterexampleAlgebra
MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleAlgebra
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
ShellFamilyTarget, homogeneityShellFamily
Used by in this Project
atomicCounterexampleRepresentation, continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra, separableCounterexampleRepresentation
AtomicCounterexampleEndpoint
MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleEndpoint
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
ShellFamilyEndpoint, homogeneityShellFamily
Used by in this Project
atomicCounterexampleEndpoint
Level 67
4 declarationsatomicCounterexampleEndpoint
MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
AtomicCounterexampleEndpoint, shellFamilyEndpoint
Used by in this Project
not_isIrreducible_of_separable
atomicCounterexampleRepresentation
MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleRepresentation
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
AtomicCounterexampleAlgebra, shellFamilyInclusion
Used by in this Project
not_isIrreducible_of_separable
continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra
MathlibAnnex.CStarAlgebra.CAR.continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
AtomicCounterexampleAlgebra, isUniqueIrreducibleModel_shellFamilyInclusion, not_finiteDimensional_shellFamilyTargetShow 1 more
Used by in this Project
cardinalMk_atomicCounterexampleAlgebra, hasDensityCharacter_atomicCounterexampleAlgebra
separableCounterexampleRepresentation
MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation
Exact source-authored def in the Naimark construction.
Immediate prerequisites in this Project
AtomicCounterexampleAlgebra, SeparableCounterexampleHilbertSpace, traceModelRepresentation
Used by in this Project
separableCounterexampleRepresentation_injective
Level 68
2 declarationsnot_isIrreducible_of_separable
MathlibAnnex.CStarAlgebra.CAR.not_isIrreducible_of_separable
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
atomicCounterexampleEndpoint, atomicCounterexampleRepresentation
Used by in this Project
atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation
separableCounterexampleRepresentation_injective
MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation_injective
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
separableCounterexampleRepresentation, traceModelRepresentation_injective
Used by in this Project
atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation, cardinalMk_atomicCounterexampleAlgebra_le_continuum
Level 69
2 declarationsatomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation
MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
nontrivial_traceHilbertSpace, not_isIrreducible_of_separable, separableCounterexampleRepresentation_injective
Used by in this Project
None in this Project
cardinalMk_atomicCounterexampleAlgebra_le_continuum
MathlibAnnex.CStarAlgebra.CAR.cardinalMk_atomicCounterexampleAlgebra_le_continuum
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
separableCounterexampleRepresentation_injective, separableSpace_separableCounterexampleHilbertSpace
Used by in this Project
cardinalMk_atomicCounterexampleAlgebra, hasDensityCharacter_atomicCounterexampleAlgebra
Level 70
2 declarationscardinalMk_atomicCounterexampleAlgebra
MathlibAnnex.CStarAlgebra.CAR.cardinalMk_atomicCounterexampleAlgebra
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
cardinalMk_atomicCounterexampleAlgebra_le_continuum, continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra
Used by in this Project
None in this Project
hasDensityCharacter_atomicCounterexampleAlgebra
MathlibAnnex.CStarAlgebra.CAR.hasDensityCharacter_atomicCounterexampleAlgebra
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
cardinalMk_atomicCounterexampleAlgebra_le_continuum, continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra
Used by in this Project
existsNaimarkCounterexampleOfDensity_continuum
Level 71
1 declarationexistsNaimarkCounterexampleOfDensity_continuum
MathlibAnnex.CStarAlgebra.CAR.existsNaimarkCounterexampleOfDensity_continuum
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
hasDensityCharacter_atomicCounterexampleAlgebra, isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion, not_isCompactOperatorModel_shellFamilyTarget
Used by in this Project
continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity
Level 72
1 declarationcontinuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity
MathlibAnnex.CStarAlgebra.CAR.continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity
Exact source-authored theorem in the Naimark construction.
Immediate prerequisites in this Project
existsNaimarkCounterexampleOfDensity_continuum
Used by in this Project
None in this Project