Blueprint Summary🔗

Overview

Total entries66completed: 52; deps incomplete: 3; incomplete code: 0; no proof: 10

Ready now4Entries with an actionable next formalization step.

Fully closed52Local code and prerequisite closure are both complete.

Actionable priorities3Entries ready now and already unlocking downstream work.

Missing informal coverage13Entries with Lean code but missing an informal statement or proof block.

Actionable priorities (3)

«cor:nonunital_gelfand_Sak_1_2_2»(Corollary)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 6proof: ready to formalize
«cor:sig_clos_of_cstar_is_wstar_Sak_1_7_9»(Corollary)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 3proof: ready to formalize
«def:strong_top»(Definition)

Ready for statement work.

stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 3

Missing informal coverage (13)

«thm:cstar_unital_iff_extreme_Sak_1_6_1»(Theorem)
Associated lean decls (3)
«prop:extr_pos_projs_Sak_1_6_2»(Proposition)
Associated lean decls (1)
- isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall
«lem:pos_cvx_cone»(Lemma)
Associated lean decls (1)
- ConvexCone.positive
«lem:selfadjoint_le_norm»(Lemma)
Associated lean decls (1)
- IsSelfAdjoint.le_algebraMap_norm_self
«thm:Banach_Alaoglu»(Theorem)
Associated lean decls (1)
- WeakDual.isCompact_closedBall
«lem:pos_iff_star_mul_self_Sak_1_4_4»(Lemma)
Associated lean decls (2)
- CStarAlgebra.nonneg_TFAE
- StarOrderedRing.nonneg_iff
«lem:pos_sa_sigma_closed_Sak_1_7_1»(Lemma)
Associated lean decls (2)
- Ultraweak.isClosed_setOf_isSelfAdjoint
- Ultraweak.isClosed_nonneg
«lem:extreme_partial_isom»(Lemma)
Associated lean decls (2)
- isStarProjection_star_mul_self_of_mem_extremePoints_unitClosedBall
- isStarProjection_self_mul_star_of_mem_extremePoints_unitClosedBall
«lem:homeo_of_cts_bij_cpt_haus»(Lemma)
Associated lean decls (1)
- isHomeomorph_iff_continuous_bijective
«lem:cauchy_schwarz»(Lemma)
Associated lean decls (1)
- PositiveLinearMap.norm_map_star_mul_le
«thm:krein_milman»(Theorem)
Associated lean decls (2)
- IsCompact.extremePoints_nonempty
- closure_convexHull_extremePoints
«prop:extr_sa_sa_unitaries_Sak_1_6_3»(Proposition)
Associated lean decls (2)
- mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary
- selfAdjoint.mem_extremePoints_unitClosedBall_iff_coe_mem_unitary
«cor:proj_sub_of_subproj»(Corollary)
Associated lean decls (1)
- IsStarProjection.le_tfae

Entry index (66)

Definitions7completed: 6; deps incomplete: 0; incomplete code: 0; no proof: 0

Propositions6completed: 4; deps incomplete: 0; incomplete code: 0; no proof: 2

Lemmas34completed: 28; deps incomplete: 2; incomplete code: 0; no proof: 4

Theorems12completed: 10; deps incomplete: 1; incomplete code: 0; no proof: 1

Corollaries7completed: 4; deps incomplete: 0; incomplete code: 0; no proof: 3

Informal-only entries11

Definition Index (7)

«def:cstar_def»(Definition)
Associated lean decls (2)
- CStarAlgebra
- NonUnitalCStarAlgebra
«def:strong_top»(Definition)
«def:sigma_top»(Definition)
Associated lean decls (1)
- Ultraweak
«def:wstar_def»(Definition)
Associated lean decls (2)
- WStarAlgebra
- Predual
«def:compatible_dual»(Definition)
Associated lean decls (1)
- LinearMap.IsCompatibleDual
«def:Mackey_top»(Definition)
Associated lean decls (1)
- Mackey
«def:weak_top»(Definition)
Associated lean decls (2)
- WeakBilin
- LinearMap.IsWeak

Theorem / Proposition / Lemma / Corollary Index (59)

«lem:sigma_eq_weak_pos_on_bdd»(Lemma)
Associated lean decls (3)
«thm:mackey_arens»(Theorem)
Associated lean decls (2)
- Mackey.range_coeLM_eq_range_bilin
- Module.dualPairing_flip_polar_polar
«cor:spec_sa_homeo_spec_cstar»(Corollary)
Associated lean decls (2)
- cfcₙ
- IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus
«thm:krein_smulian»(Theorem)
Associated lean decls (3)
«lem:zorn_base»(Lemma)
Associated lean decls (1)
- Ultraweak.exists_maximal_continuous_mul_right
«lem:directed_sup_proj»(Lemma)
Associated lean decls (1)
- Ultraweak.isStarProjection_of_isLUB
«thm:cstar_unital_iff_extreme_Sak_1_6_1»(Theorem)
Associated lean decls (3)
«lem:cts_fns_ge_zero_le_one_directed»(Lemma)
«lem:proj_sub_pos_iff_comm_eq_self»(Lemma)
Associated lean decls (1)
- IsStarProjection.le_tfae
«prop:loc_cvx_result»(Proposition)
Associated lean decls (2)
- Ultraweak.continuous_iff_exists_eq
- Ultraweak.continuous_iff_mem_range
«lem:cut_down_of_wstar»(Lemma)
Associated lean decls (2)
- IsStarProjection.Corner.instCStarAlgebra
- IsStarProjection.Corner.instPredual
«prop:extr_pos_projs_Sak_1_6_2»(Proposition)
Associated lean decls (1)
- isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall
«lem:pos_cvx_cone»(Lemma)
Associated lean decls (1)
- ConvexCone.positive
«thm:sigma_le_s_le_tau»(Theorem)
«lem:bdd_sigma_cts_iff_bdd_s_cts_Sak_1_8_10»(Lemma)
«lem:fake_approx_unit»(Lemma)
«lem:weak_dual»(Lemma)
Associated lean decls (2)
- LinearMap.IsWeak.eval_surjective
- LinearMap.IsWeak.rightDualEquiv
«cor:sig_clos_of_cstar_is_wstar_Sak_1_7_9»(Corollary)
«lem:corner_comparison»(Lemma)
Associated lean decls (2)
- Ultraweak.map_le_map_of_forall_lt
- PositiveLinearMap.le_of_le_on_isStarProjection
«cor:nonunital_gelfand_Sak_1_2_2»(Corollary)
«lem:wstar_of_masa»(Lemma)
«prop:proj_compl_lat_wstar_Sak_1_10_2»(Proposition)
«lem:uw_pos_sep_pts»(Lemma)
Associated lean decls (1)
- Ultraweak.ext_positiveCLM
«thm:bipolar»(Theorem)
Associated lean decls (2)
- LinearMap.flip_polar_polar
- LinearMap.IsCompatibleDual.flip_polar_polar
«lem:sigma_closed_star_subalg_wstar»(Lemma)
Associated lean decls (2)
- Ultraweak.predualOfIsClosed
- Submodule.equivDualQuotientPolarSubmodule
«lem:fin_lin_approx_of_stonean_Sak_1_3_1»(Lemma)
Associated lean decls (2)
- ContinuousMap.instFiniteSpectrum
- CStarAlgebra.FiniteSpectrum.mem_closure_hull_isStarProjection
«lem:spec_masa_wstar_stonean_Sak_1_7_5»(Lemma)
Associated lean decls (1)
- StarSubalgebra.IsMasa.extremallyDisconnected_characterSpace
«lem:dominated_sigma_cts»(Lemma)
Associated lean decls (1)
- Ultraweak.continuous_of_norm_sq_le
«lem:non_pos_elem_neg_for_some_state_Sak_1_7_2»(Lemma)
Associated lean decls (1)
- Ultraweak.exists_positiveCLM_apply_lt_zero
«lem:selfadjoint_le_norm»(Lemma)
Associated lean decls (1)
- IsSelfAdjoint.le_algebraMap_norm_self
«thm:Banach_Alaoglu»(Theorem)
Associated lean decls (1)
- WeakDual.isCompact_closedBall
«lem:wstar_pos_approx_proj»(Lemma)
Associated lean decls (3)
«thm:predual_unique»(Theorem)
Associated lean decls (2)
- Ultraweak.continuousLinearEquivOfPredual
- Predual.uniqueEquiv
«thm:sigma_cts_of_normal_Sak_1_13_2»(Theorem)
Associated lean decls (2)
- Ultraweak.continuous_of_scottContinuousOn
- Ultraweak.continuous_of_scottContinuousOn_chains
«lem:cut_down_sigma_closed_cts»(Lemma)
Associated lean decls (1)
- IsStarProjection.isClosed_cornerSubmodule_of_ultraweak
«lem:sigma_cont_of_normal_Sak_1_7_4»(Theorem)
Associated lean decls (2)
- Ultraweak.DirectedOn.exists_isLUB
- Ultraweak.DirectedOn.isLUB_star_right_conjugate
«lem:left_mul_proj_right_mul_proj_sig_cts_Sak_1_7_7»(Lemma)
Associated lean decls (1)
- Ultraweak.continuous_mul_left_of_isStarProjection
«thm:sakai_normal_iff»(Theorem)
Associated lean decls (2)
- Ultraweak.positive_tfae
- Ultraweak.scottContinuous_of_scottContinuousOn_chains
«cor:bipolar_submodule»(Corollary)
Associated lean decls (2)
- LinearMap.IsWeak.flip_polarSubmodule_polarSubmodule
- LinearMap.IsCompatibleDual.flip_polarSubmodule_polarSubmodule
«lem:pos_iff_star_mul_self_Sak_1_4_4»(Lemma)
Associated lean decls (2)
- CStarAlgebra.nonneg_TFAE
- StarOrderedRing.nonneg_iff
«lem:pos_sa_sigma_closed_Sak_1_7_1»(Lemma)
Associated lean decls (2)
- Ultraweak.isClosed_setOf_isSelfAdjoint
- Ultraweak.isClosed_nonneg
«lem:extreme_partial_isom»(Lemma)
Associated lean decls (2)
- isStarProjection_star_mul_self_of_mem_extremePoints_unitClosedBall
- isStarProjection_self_mul_star_of_mem_extremePoints_unitClosedBall
«prop:one_sided_ideals_in_wstar_proj_Sak_1_10_1»(Proposition)
«lem:homeo_of_cts_bij_cpt_haus»(Lemma)
Associated lean decls (1)
- isHomeomorph_iff_continuous_bijective
«lem:cauchy_schwarz»(Lemma)
Associated lean decls (1)
- PositiveLinearMap.norm_map_star_mul_le
«lem:star_left_mul_right_mul_sig_cts_Sak_1_7_8»(Lemma)
Associated lean decls (2)
- Ultraweak.instSeparatelyContinuousMul
- Ultraweak.instIsSemitopologicalRing
«lem:wstar_unital»(Lemma)
Associated lean decls (3)
«lem:msr_th_lemma»(Lemma)
Associated lean decls (1)
- Ultraweak.exists_forall_lt
«lem:star_conj_pos»(Corollary)
Associated lean decls (1)
- star_left_conjugate_nonneg
«prop:stonean_of_cts_fcns_incr_cond_complete_Sak_1_3_2»(Proposition)
Associated lean decls (1)
- ExtremallyDisconnected.ofConditionallyCompletePartialOrderSupContinuousMap
«cor:sigma_eq_s_on_ball»(Corollary)
«thm:comm_cstar_cts_fcns_Sak_1_2_1»(Theorem)
Associated lean decls (1)
- gelfandStarTransform
«thm:krein_milman»(Theorem)
Associated lean decls (2)
- IsCompact.extremePoints_nonempty
- closure_convexHull_extremePoints
«lem:proj_le_one»(Lemma)
Associated lean decls (1)
- IsStarProjection.le_one
«prop:extr_sa_sa_unitaries_Sak_1_6_3»(Proposition)
Associated lean decls (2)
- mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary
- selfAdjoint.mem_extremePoints_unitClosedBall_iff_coe_mem_unitary
«lem:star_pres_norm_Sak_1_1_6»(Lemma)
Associated lean decls (1)
- CStarRing.to_normedStarGroup
«lem:exists_uw_ge_normal»(Lemma)
Associated lean decls (1)
- Ultraweak.exists_lt_of_ne_zero
«cor:proj_sub_of_subproj»(Corollary)
Associated lean decls (1)
- IsStarProjection.le_tfae
«lem:one_is_extreme»(Lemma)
Associated lean decls (1)
- CStarAlgebra.one_mem_extremePoints_unitClosedBall

Dependency insights

Statement-used entries61Entries reused in statement dependencies.

Most used in statements (61)

«def:sigma_top»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 17proof uses: 0direct uses: 17downstream unlocks: 30
Associated lean decls (1)
- Ultraweak
«def:cstar_def»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 44
Associated lean decls (2)
- CStarAlgebra
- NonUnitalCStarAlgebra
«def:weak_top»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 37
Associated lean decls (2)
- WeakBilin
- LinearMap.IsWeak
«def:compatible_dual»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 34
Associated lean decls (1)
- LinearMap.IsCompatibleDual
«lem:sigma_cont_of_normal_Sak_1_7_4»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 15
Associated lean decls (2)
- Ultraweak.DirectedOn.exists_isLUB
- Ultraweak.DirectedOn.isLUB_star_right_conjugate
«prop:loc_cvx_result»(Proposition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 12
Associated lean decls (2)
- Ultraweak.continuous_iff_exists_eq
- Ultraweak.continuous_iff_mem_range
«lem:star_left_mul_right_mul_sig_cts_Sak_1_7_8»(Lemma)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 11
Associated lean decls (2)
- Ultraweak.instSeparatelyContinuousMul
- Ultraweak.instIsSemitopologicalRing
«thm:krein_smulian»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 24
Associated lean decls (3)
«thm:comm_cstar_cts_fcns_Sak_1_2_1»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 23
Associated lean decls (1)
- gelfandStarTransform
«lem:selfadjoint_le_norm»(Lemma)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 20
Associated lean decls (1)
- IsSelfAdjoint.le_algebraMap_norm_self
Show all 51 more statement-used entries
- «def:wstar_def»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 32
  Associated lean decls (2)
  - WStarAlgebra
  - Predual
- «thm:Banach_Alaoglu»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 26
  Associated lean decls (1)
  - WeakDual.isCompact_closedBall
- «lem:pos_sa_sigma_closed_Sak_1_7_1»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 23
  Associated lean decls (2)
  - Ultraweak.isClosed_setOf_isSelfAdjoint
  - Ultraweak.isClosed_nonneg
- «lem:cauchy_schwarz»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 16
  Associated lean decls (1)
  - PositiveLinearMap.norm_map_star_mul_le
- «lem:proj_sub_pos_iff_comm_eq_self»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 8
  Associated lean decls (1)
  - IsStarProjection.le_tfae
- «lem:weak_dual»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 22
  Associated lean decls (2)
  - LinearMap.IsWeak.eval_surjective
  - LinearMap.IsWeak.rightDualEquiv
- «lem:homeo_of_cts_bij_cpt_haus»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 19
  Associated lean decls (1)
  - isHomeomorph_iff_continuous_bijective
- «lem:non_pos_elem_neg_for_some_state_Sak_1_7_2»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 19
  Associated lean decls (1)
  - Ultraweak.exists_positiveCLM_apply_lt_zero
- «lem:star_conj_pos»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 18
  Associated lean decls (1)
  - star_left_conjugate_nonneg
- «lem:uw_pos_sep_pts»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 18
  Associated lean decls (1)
  - Ultraweak.ext_positiveCLM
- «lem:sigma_eq_weak_pos_on_bdd»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 16
  Associated lean decls (3)
- «lem:cut_down_sigma_closed_cts»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 15
  Associated lean decls (1)
  - IsStarProjection.isClosed_cornerSubmodule_of_ultraweak
- «lem:wstar_pos_approx_proj»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 13
  Associated lean decls (3)
- «lem:left_mul_proj_right_mul_proj_sig_cts_Sak_1_7_7»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 12
  Associated lean decls (1)
  - Ultraweak.continuous_mul_left_of_isStarProjection
- «thm:bipolar»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
  Associated lean decls (2)
  - LinearMap.flip_polar_polar
  - LinearMap.IsCompatibleDual.flip_polar_polar
- «cor:proj_sub_of_subproj»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - IsStarProjection.le_tfae
- «lem:directed_sup_proj»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - Ultraweak.isStarProjection_of_isLUB
- «def:Mackey_top»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (1)
  - Mackey
- «cor:sig_clos_of_cstar_is_wstar_Sak_1_7_9»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
- «lem:pos_cvx_cone»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 20
  Associated lean decls (1)
  - ConvexCone.positive
- «lem:pos_iff_star_mul_self_Sak_1_4_4»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
  Associated lean decls (2)
  - CStarAlgebra.nonneg_TFAE
  - StarOrderedRing.nonneg_iff
- «cor:spec_sa_homeo_spec_cstar»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 15
  Associated lean decls (2)
  - cfcₙ
  - IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus
- «prop:stonean_of_cts_fcns_incr_cond_complete_Sak_1_3_2»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 15
  Associated lean decls (1)
  - ExtremallyDisconnected.ofConditionallyCompletePartialOrderSupContinuousMap
- «lem:fin_lin_approx_of_stonean_Sak_1_3_1»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 14
  Associated lean decls (2)
  - ContinuousMap.instFiniteSpectrum
  - CStarAlgebra.FiniteSpectrum.mem_closure_hull_isStarProjection
- «lem:spec_masa_wstar_stonean_Sak_1_7_5»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 14
  Associated lean decls (1)
  - StarSubalgebra.IsMasa.extremallyDisconnected_characterSpace
- «lem:proj_le_one»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - IsStarProjection.le_one
- «cor:bipolar_submodule»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (2)
  - LinearMap.IsWeak.flip_polarSubmodule_polarSubmodule
  - LinearMap.IsCompatibleDual.flip_polarSubmodule_polarSubmodule
- «cor:nonunital_gelfand_Sak_1_2_2»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
- «lem:fake_approx_unit»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
- «lem:sigma_closed_star_subalg_wstar»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (2)
  - Ultraweak.predualOfIsClosed
  - Submodule.equivDualQuotientPolarSubmodule
- «lem:star_pres_norm_Sak_1_1_6»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - CStarRing.to_normedStarGroup
- «lem:cut_down_of_wstar»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - IsStarProjection.Corner.instCStarAlgebra
  - IsStarProjection.Corner.instPredual
- «lem:extreme_partial_isom»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - isStarProjection_star_mul_self_of_mem_extremePoints_unitClosedBall
  - isStarProjection_self_mul_star_of_mem_extremePoints_unitClosedBall
- «lem:one_is_extreme»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - CStarAlgebra.one_mem_extremePoints_unitClosedBall
- «prop:extr_pos_projs_Sak_1_6_2»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall
- «def:strong_top»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
- «lem:corner_comparison»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - Ultraweak.map_le_map_of_forall_lt
  - PositiveLinearMap.le_of_le_on_isStarProjection
- «lem:dominated_sigma_cts»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Ultraweak.continuous_of_norm_sq_le
- «lem:exists_uw_ge_normal»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Ultraweak.exists_lt_of_ne_zero
- «lem:msr_th_lemma»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Ultraweak.exists_forall_lt
- «lem:zorn_base»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Ultraweak.exists_maximal_continuous_mul_right
- «prop:extr_sa_sa_unitaries_Sak_1_6_3»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary
  - selfAdjoint.mem_extremePoints_unitClosedBall_iff_coe_mem_unitary
- «thm:cstar_unital_iff_extreme_Sak_1_6_1»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (3)
- «thm:krein_milman»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - IsCompact.extremePoints_nonempty
  - closure_convexHull_extremePoints
- «thm:mackey_arens»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - Mackey.range_coeLM_eq_range_bilin
  - Module.dualPairing_flip_polar_polar
- «lem:wstar_unital»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (3)
- «thm:sigma_cts_of_normal_Sak_1_13_2»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - Ultraweak.continuous_of_scottContinuousOn
  - Ultraweak.continuous_of_scottContinuousOn_chains
- «thm:sigma_le_s_le_tau»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
- «cor:sigma_eq_s_on_ball»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
- «prop:one_sided_ideals_in_wstar_proj_Sak_1_10_1»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
- «thm:sakai_normal_iff»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - Ultraweak.positive_tfae
  - Ultraweak.scottContinuous_of_scottContinuousOn_chains

Metadata

Tags in use1Distinct tags currently attached to blueprint entries.

Tag rollups (1)

tag: mathlib

entries: 13actionable: 0quick wins: 0linked PRs: 0

Metadata audit

Missing owner66

Missing effort66

Untagged53

Missing owner (66)

«cor:bipolar_submodule»(Corollary)

Missing owner metadata.
Associated lean decls (2)
- LinearMap.IsWeak.flip_polarSubmodule_polarSubmodule
- LinearMap.IsCompatibleDual.flip_polarSubmodule_polarSubmodule
«cor:nonunital_gelfand_Sak_1_2_2»(Corollary)

Missing owner metadata.
«cor:proj_sub_of_subproj»(Corollary)

Missing owner metadata.
Associated lean decls (1)
- IsStarProjection.le_tfae
«cor:sig_clos_of_cstar_is_wstar_Sak_1_7_9»(Corollary)

Missing owner metadata.
«cor:sigma_eq_s_on_ball»(Corollary)

Missing owner metadata.
«cor:spec_sa_homeo_spec_cstar»(Corollary)

Missing owner metadata.

tag: mathlib
Associated lean decls (2)
- cfcₙ
- IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus
«def:Mackey_top»(Definition)

Missing owner metadata.
Associated lean decls (1)
- Mackey
«def:compatible_dual»(Definition)

Missing owner metadata.
Associated lean decls (1)
- LinearMap.IsCompatibleDual
«def:cstar_def»(Definition)

Missing owner metadata.

tag: mathlib
Associated lean decls (2)
- CStarAlgebra
- NonUnitalCStarAlgebra
«def:sigma_top»(Definition)

Missing owner metadata.
Associated lean decls (1)
- Ultraweak
Show all 56 more entries missing owner
- «def:strong_top»(Definition)
  
  Missing owner metadata.
- «def:weak_top»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - WeakBilin
  - LinearMap.IsWeak
- «def:wstar_def»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - WStarAlgebra
  - Predual
- «lem:bdd_sigma_cts_iff_bdd_s_cts_Sak_1_8_10»(Lemma)
  
  Missing owner metadata.
- «lem:cauchy_schwarz»(Lemma)
  
  Missing owner metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - PositiveLinearMap.norm_map_star_mul_le
- «lem:corner_comparison»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Ultraweak.map_le_map_of_forall_lt
  - PositiveLinearMap.le_of_le_on_isStarProjection
- «lem:cts_fns_ge_zero_le_one_directed»(Lemma)
  
  Missing owner metadata.
- «lem:cut_down_of_wstar»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - IsStarProjection.Corner.instCStarAlgebra
  - IsStarProjection.Corner.instPredual
- «lem:cut_down_sigma_closed_cts»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - IsStarProjection.isClosed_cornerSubmodule_of_ultraweak
- «lem:directed_sup_proj»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Ultraweak.isStarProjection_of_isLUB
- «lem:dominated_sigma_cts»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Ultraweak.continuous_of_norm_sq_le
- «lem:exists_uw_ge_normal»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Ultraweak.exists_lt_of_ne_zero
- «lem:extreme_partial_isom»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - isStarProjection_star_mul_self_of_mem_extremePoints_unitClosedBall
  - isStarProjection_self_mul_star_of_mem_extremePoints_unitClosedBall
- «lem:fake_approx_unit»(Lemma)
  
  Missing owner metadata.
- «lem:fin_lin_approx_of_stonean_Sak_1_3_1»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - ContinuousMap.instFiniteSpectrum
  - CStarAlgebra.FiniteSpectrum.mem_closure_hull_isStarProjection
- «lem:homeo_of_cts_bij_cpt_haus»(Lemma)
  
  Missing owner metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - isHomeomorph_iff_continuous_bijective
- «lem:left_mul_proj_right_mul_proj_sig_cts_Sak_1_7_7»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Ultraweak.continuous_mul_left_of_isStarProjection
- «lem:msr_th_lemma»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Ultraweak.exists_forall_lt
- «lem:non_pos_elem_neg_for_some_state_Sak_1_7_2»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Ultraweak.exists_positiveCLM_apply_lt_zero
- «lem:one_is_extreme»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - CStarAlgebra.one_mem_extremePoints_unitClosedBall
- «lem:pos_cvx_cone»(Lemma)
  
  Missing owner metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - ConvexCone.positive
- «lem:pos_iff_star_mul_self_Sak_1_4_4»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - CStarAlgebra.nonneg_TFAE
  - StarOrderedRing.nonneg_iff
- «lem:pos_sa_sigma_closed_Sak_1_7_1»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Ultraweak.isClosed_setOf_isSelfAdjoint
  - Ultraweak.isClosed_nonneg
- «lem:proj_le_one»(Lemma)
  
  Missing owner metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - IsStarProjection.le_one
- «lem:proj_sub_pos_iff_comm_eq_self»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - IsStarProjection.le_tfae
- «lem:selfadjoint_le_norm»(Lemma)
  
  Missing owner metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - IsSelfAdjoint.le_algebraMap_norm_self
- «lem:sigma_closed_star_subalg_wstar»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Ultraweak.predualOfIsClosed
  - Submodule.equivDualQuotientPolarSubmodule
- «lem:sigma_cont_of_normal_Sak_1_7_4»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Ultraweak.DirectedOn.exists_isLUB
  - Ultraweak.DirectedOn.isLUB_star_right_conjugate
- «lem:sigma_eq_weak_pos_on_bdd»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:spec_masa_wstar_stonean_Sak_1_7_5»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - StarSubalgebra.IsMasa.extremallyDisconnected_characterSpace
- «lem:star_conj_pos»(Corollary)
  
  Missing owner metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - star_left_conjugate_nonneg
- «lem:star_left_mul_right_mul_sig_cts_Sak_1_7_8»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Ultraweak.instSeparatelyContinuousMul
  - Ultraweak.instIsSemitopologicalRing
- «lem:star_pres_norm_Sak_1_1_6»(Lemma)
  
  Missing owner metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - CStarRing.to_normedStarGroup
- «lem:uw_pos_sep_pts»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Ultraweak.ext_positiveCLM
- «lem:weak_dual»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LinearMap.IsWeak.eval_surjective
  - LinearMap.IsWeak.rightDualEquiv
- «lem:wstar_of_masa»(Lemma)
  
  Missing owner metadata.
- «lem:wstar_pos_approx_proj»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:wstar_unital»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:zorn_base»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Ultraweak.exists_maximal_continuous_mul_right
- «prop:extr_pos_projs_Sak_1_6_2»(Proposition)
  
  Missing owner metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall
- «prop:extr_sa_sa_unitaries_Sak_1_6_3»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary
  - selfAdjoint.mem_extremePoints_unitClosedBall_iff_coe_mem_unitary
- «prop:loc_cvx_result»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Ultraweak.continuous_iff_exists_eq
  - Ultraweak.continuous_iff_mem_range
- «prop:one_sided_ideals_in_wstar_proj_Sak_1_10_1»(Proposition)
  
  Missing owner metadata.
- «prop:proj_compl_lat_wstar_Sak_1_10_2»(Proposition)
  
  Missing owner metadata.
- «prop:stonean_of_cts_fcns_incr_cond_complete_Sak_1_3_2»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - ExtremallyDisconnected.ofConditionallyCompletePartialOrderSupContinuousMap
- «thm:Banach_Alaoglu»(Theorem)
  
  Missing owner metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - WeakDual.isCompact_closedBall
- «thm:bipolar»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LinearMap.flip_polar_polar
  - LinearMap.IsCompatibleDual.flip_polar_polar
- «thm:comm_cstar_cts_fcns_Sak_1_2_1»(Theorem)
  
  Missing owner metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - gelfandStarTransform
- «thm:cstar_unital_iff_extreme_Sak_1_6_1»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- «thm:krein_milman»(Theorem)
  
  Missing owner metadata.
  
  tag: mathlib
  Associated lean decls (2)
  - IsCompact.extremePoints_nonempty
  - closure_convexHull_extremePoints
- «thm:krein_smulian»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- «thm:mackey_arens»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Mackey.range_coeLM_eq_range_bilin
  - Module.dualPairing_flip_polar_polar
- «thm:predual_unique»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Ultraweak.continuousLinearEquivOfPredual
  - Predual.uniqueEquiv
- «thm:sakai_normal_iff»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Ultraweak.positive_tfae
  - Ultraweak.scottContinuous_of_scottContinuousOn_chains
- «thm:sigma_cts_of_normal_Sak_1_13_2»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Ultraweak.continuous_of_scottContinuousOn
  - Ultraweak.continuous_of_scottContinuousOn_chains
- «thm:sigma_le_s_le_tau»(Theorem)
  
  Missing owner metadata.

Missing effort (66)

«cor:bipolar_submodule»(Corollary)

Missing effort metadata.
Associated lean decls (2)
- LinearMap.IsWeak.flip_polarSubmodule_polarSubmodule
- LinearMap.IsCompatibleDual.flip_polarSubmodule_polarSubmodule
«cor:nonunital_gelfand_Sak_1_2_2»(Corollary)

Missing effort metadata.
«cor:proj_sub_of_subproj»(Corollary)

Missing effort metadata.
Associated lean decls (1)
- IsStarProjection.le_tfae
«cor:sig_clos_of_cstar_is_wstar_Sak_1_7_9»(Corollary)

Missing effort metadata.
«cor:sigma_eq_s_on_ball»(Corollary)

Missing effort metadata.
«cor:spec_sa_homeo_spec_cstar»(Corollary)

Missing effort metadata.

tag: mathlib
Associated lean decls (2)
- cfcₙ
- IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus
«def:Mackey_top»(Definition)

Missing effort metadata.
Associated lean decls (1)
- Mackey
«def:compatible_dual»(Definition)

Missing effort metadata.
Associated lean decls (1)
- LinearMap.IsCompatibleDual
«def:cstar_def»(Definition)

Missing effort metadata.

tag: mathlib
Associated lean decls (2)
- CStarAlgebra
- NonUnitalCStarAlgebra
«def:sigma_top»(Definition)

Missing effort metadata.
Associated lean decls (1)
- Ultraweak
Show all 56 more entries missing effort
- «def:strong_top»(Definition)
  
  Missing effort metadata.
- «def:weak_top»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - WeakBilin
  - LinearMap.IsWeak
- «def:wstar_def»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - WStarAlgebra
  - Predual
- «lem:bdd_sigma_cts_iff_bdd_s_cts_Sak_1_8_10»(Lemma)
  
  Missing effort metadata.
- «lem:cauchy_schwarz»(Lemma)
  
  Missing effort metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - PositiveLinearMap.norm_map_star_mul_le
- «lem:corner_comparison»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Ultraweak.map_le_map_of_forall_lt
  - PositiveLinearMap.le_of_le_on_isStarProjection
- «lem:cts_fns_ge_zero_le_one_directed»(Lemma)
  
  Missing effort metadata.
- «lem:cut_down_of_wstar»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - IsStarProjection.Corner.instCStarAlgebra
  - IsStarProjection.Corner.instPredual
- «lem:cut_down_sigma_closed_cts»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - IsStarProjection.isClosed_cornerSubmodule_of_ultraweak
- «lem:directed_sup_proj»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Ultraweak.isStarProjection_of_isLUB
- «lem:dominated_sigma_cts»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Ultraweak.continuous_of_norm_sq_le
- «lem:exists_uw_ge_normal»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Ultraweak.exists_lt_of_ne_zero
- «lem:extreme_partial_isom»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - isStarProjection_star_mul_self_of_mem_extremePoints_unitClosedBall
  - isStarProjection_self_mul_star_of_mem_extremePoints_unitClosedBall
- «lem:fake_approx_unit»(Lemma)
  
  Missing effort metadata.
- «lem:fin_lin_approx_of_stonean_Sak_1_3_1»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - ContinuousMap.instFiniteSpectrum
  - CStarAlgebra.FiniteSpectrum.mem_closure_hull_isStarProjection
- «lem:homeo_of_cts_bij_cpt_haus»(Lemma)
  
  Missing effort metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - isHomeomorph_iff_continuous_bijective
- «lem:left_mul_proj_right_mul_proj_sig_cts_Sak_1_7_7»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Ultraweak.continuous_mul_left_of_isStarProjection
- «lem:msr_th_lemma»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Ultraweak.exists_forall_lt
- «lem:non_pos_elem_neg_for_some_state_Sak_1_7_2»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Ultraweak.exists_positiveCLM_apply_lt_zero
- «lem:one_is_extreme»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - CStarAlgebra.one_mem_extremePoints_unitClosedBall
- «lem:pos_cvx_cone»(Lemma)
  
  Missing effort metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - ConvexCone.positive
- «lem:pos_iff_star_mul_self_Sak_1_4_4»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - CStarAlgebra.nonneg_TFAE
  - StarOrderedRing.nonneg_iff
- «lem:pos_sa_sigma_closed_Sak_1_7_1»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Ultraweak.isClosed_setOf_isSelfAdjoint
  - Ultraweak.isClosed_nonneg
- «lem:proj_le_one»(Lemma)
  
  Missing effort metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - IsStarProjection.le_one
- «lem:proj_sub_pos_iff_comm_eq_self»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - IsStarProjection.le_tfae
- «lem:selfadjoint_le_norm»(Lemma)
  
  Missing effort metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - IsSelfAdjoint.le_algebraMap_norm_self
- «lem:sigma_closed_star_subalg_wstar»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Ultraweak.predualOfIsClosed
  - Submodule.equivDualQuotientPolarSubmodule
- «lem:sigma_cont_of_normal_Sak_1_7_4»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Ultraweak.DirectedOn.exists_isLUB
  - Ultraweak.DirectedOn.isLUB_star_right_conjugate
- «lem:sigma_eq_weak_pos_on_bdd»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:spec_masa_wstar_stonean_Sak_1_7_5»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - StarSubalgebra.IsMasa.extremallyDisconnected_characterSpace
- «lem:star_conj_pos»(Corollary)
  
  Missing effort metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - star_left_conjugate_nonneg
- «lem:star_left_mul_right_mul_sig_cts_Sak_1_7_8»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Ultraweak.instSeparatelyContinuousMul
  - Ultraweak.instIsSemitopologicalRing
- «lem:star_pres_norm_Sak_1_1_6»(Lemma)
  
  Missing effort metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - CStarRing.to_normedStarGroup
- «lem:uw_pos_sep_pts»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Ultraweak.ext_positiveCLM
- «lem:weak_dual»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LinearMap.IsWeak.eval_surjective
  - LinearMap.IsWeak.rightDualEquiv
- «lem:wstar_of_masa»(Lemma)
  
  Missing effort metadata.
- «lem:wstar_pos_approx_proj»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:wstar_unital»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:zorn_base»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Ultraweak.exists_maximal_continuous_mul_right
- «prop:extr_pos_projs_Sak_1_6_2»(Proposition)
  
  Missing effort metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall
- «prop:extr_sa_sa_unitaries_Sak_1_6_3»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary
  - selfAdjoint.mem_extremePoints_unitClosedBall_iff_coe_mem_unitary
- «prop:loc_cvx_result»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Ultraweak.continuous_iff_exists_eq
  - Ultraweak.continuous_iff_mem_range
- «prop:one_sided_ideals_in_wstar_proj_Sak_1_10_1»(Proposition)
  
  Missing effort metadata.
- «prop:proj_compl_lat_wstar_Sak_1_10_2»(Proposition)
  
  Missing effort metadata.
- «prop:stonean_of_cts_fcns_incr_cond_complete_Sak_1_3_2»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - ExtremallyDisconnected.ofConditionallyCompletePartialOrderSupContinuousMap
- «thm:Banach_Alaoglu»(Theorem)
  
  Missing effort metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - WeakDual.isCompact_closedBall
- «thm:bipolar»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LinearMap.flip_polar_polar
  - LinearMap.IsCompatibleDual.flip_polar_polar
- «thm:comm_cstar_cts_fcns_Sak_1_2_1»(Theorem)
  
  Missing effort metadata.
  
  tag: mathlib
  Associated lean decls (1)
  - gelfandStarTransform
- «thm:cstar_unital_iff_extreme_Sak_1_6_1»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- «thm:krein_milman»(Theorem)
  
  Missing effort metadata.
  
  tag: mathlib
  Associated lean decls (2)
  - IsCompact.extremePoints_nonempty
  - closure_convexHull_extremePoints
- «thm:krein_smulian»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- «thm:mackey_arens»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Mackey.range_coeLM_eq_range_bilin
  - Module.dualPairing_flip_polar_polar
- «thm:predual_unique»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Ultraweak.continuousLinearEquivOfPredual
  - Predual.uniqueEquiv
- «thm:sakai_normal_iff»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Ultraweak.positive_tfae
  - Ultraweak.scottContinuous_of_scottContinuousOn_chains
- «thm:sigma_cts_of_normal_Sak_1_13_2»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Ultraweak.continuous_of_scottContinuousOn
  - Ultraweak.continuous_of_scottContinuousOn_chains
- «thm:sigma_le_s_le_tau»(Theorem)
  
  Missing effort metadata.

Untagged (53)

«cor:bipolar_submodule»(Corollary)

Missing tag metadata.
Associated lean decls (2)
- LinearMap.IsWeak.flip_polarSubmodule_polarSubmodule
- LinearMap.IsCompatibleDual.flip_polarSubmodule_polarSubmodule
«cor:nonunital_gelfand_Sak_1_2_2»(Corollary)

Missing tag metadata.
«cor:proj_sub_of_subproj»(Corollary)

Missing tag metadata.
Associated lean decls (1)
- IsStarProjection.le_tfae
«cor:sig_clos_of_cstar_is_wstar_Sak_1_7_9»(Corollary)

Missing tag metadata.
«cor:sigma_eq_s_on_ball»(Corollary)

Missing tag metadata.
«def:Mackey_top»(Definition)

Missing tag metadata.
Associated lean decls (1)
- Mackey
«def:compatible_dual»(Definition)

Missing tag metadata.
Associated lean decls (1)
- LinearMap.IsCompatibleDual
«def:sigma_top»(Definition)

Missing tag metadata.
Associated lean decls (1)
- Ultraweak
«def:strong_top»(Definition)

Missing tag metadata.
«def:weak_top»(Definition)

Missing tag metadata.
Associated lean decls (2)
- WeakBilin
- LinearMap.IsWeak
Show all 43 more untagged entries
- «def:wstar_def»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - WStarAlgebra
  - Predual
- «lem:bdd_sigma_cts_iff_bdd_s_cts_Sak_1_8_10»(Lemma)
  
  Missing tag metadata.
- «lem:corner_comparison»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Ultraweak.map_le_map_of_forall_lt
  - PositiveLinearMap.le_of_le_on_isStarProjection
- «lem:cts_fns_ge_zero_le_one_directed»(Lemma)
  
  Missing tag metadata.
- «lem:cut_down_of_wstar»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - IsStarProjection.Corner.instCStarAlgebra
  - IsStarProjection.Corner.instPredual
- «lem:cut_down_sigma_closed_cts»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - IsStarProjection.isClosed_cornerSubmodule_of_ultraweak
- «lem:directed_sup_proj»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Ultraweak.isStarProjection_of_isLUB
- «lem:dominated_sigma_cts»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Ultraweak.continuous_of_norm_sq_le
- «lem:exists_uw_ge_normal»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Ultraweak.exists_lt_of_ne_zero
- «lem:extreme_partial_isom»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - isStarProjection_star_mul_self_of_mem_extremePoints_unitClosedBall
  - isStarProjection_self_mul_star_of_mem_extremePoints_unitClosedBall
- «lem:fake_approx_unit»(Lemma)
  
  Missing tag metadata.
- «lem:fin_lin_approx_of_stonean_Sak_1_3_1»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - ContinuousMap.instFiniteSpectrum
  - CStarAlgebra.FiniteSpectrum.mem_closure_hull_isStarProjection
- «lem:left_mul_proj_right_mul_proj_sig_cts_Sak_1_7_7»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Ultraweak.continuous_mul_left_of_isStarProjection
- «lem:msr_th_lemma»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Ultraweak.exists_forall_lt
- «lem:non_pos_elem_neg_for_some_state_Sak_1_7_2»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Ultraweak.exists_positiveCLM_apply_lt_zero
- «lem:one_is_extreme»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - CStarAlgebra.one_mem_extremePoints_unitClosedBall
- «lem:pos_iff_star_mul_self_Sak_1_4_4»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - CStarAlgebra.nonneg_TFAE
  - StarOrderedRing.nonneg_iff
- «lem:pos_sa_sigma_closed_Sak_1_7_1»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Ultraweak.isClosed_setOf_isSelfAdjoint
  - Ultraweak.isClosed_nonneg
- «lem:proj_sub_pos_iff_comm_eq_self»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - IsStarProjection.le_tfae
- «lem:sigma_closed_star_subalg_wstar»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Ultraweak.predualOfIsClosed
  - Submodule.equivDualQuotientPolarSubmodule
- «lem:sigma_cont_of_normal_Sak_1_7_4»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Ultraweak.DirectedOn.exists_isLUB
  - Ultraweak.DirectedOn.isLUB_star_right_conjugate
- «lem:sigma_eq_weak_pos_on_bdd»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:spec_masa_wstar_stonean_Sak_1_7_5»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - StarSubalgebra.IsMasa.extremallyDisconnected_characterSpace
- «lem:star_left_mul_right_mul_sig_cts_Sak_1_7_8»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Ultraweak.instSeparatelyContinuousMul
  - Ultraweak.instIsSemitopologicalRing
- «lem:uw_pos_sep_pts»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Ultraweak.ext_positiveCLM
- «lem:weak_dual»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LinearMap.IsWeak.eval_surjective
  - LinearMap.IsWeak.rightDualEquiv
- «lem:wstar_of_masa»(Lemma)
  
  Missing tag metadata.
- «lem:wstar_pos_approx_proj»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:wstar_unital»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:zorn_base»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Ultraweak.exists_maximal_continuous_mul_right
- «prop:extr_sa_sa_unitaries_Sak_1_6_3»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary
  - selfAdjoint.mem_extremePoints_unitClosedBall_iff_coe_mem_unitary
- «prop:loc_cvx_result»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Ultraweak.continuous_iff_exists_eq
  - Ultraweak.continuous_iff_mem_range
- «prop:one_sided_ideals_in_wstar_proj_Sak_1_10_1»(Proposition)
  
  Missing tag metadata.
- «prop:proj_compl_lat_wstar_Sak_1_10_2»(Proposition)
  
  Missing tag metadata.
- «prop:stonean_of_cts_fcns_incr_cond_complete_Sak_1_3_2»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - ExtremallyDisconnected.ofConditionallyCompletePartialOrderSupContinuousMap
- «thm:bipolar»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LinearMap.flip_polar_polar
  - LinearMap.IsCompatibleDual.flip_polar_polar
- «thm:cstar_unital_iff_extreme_Sak_1_6_1»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- «thm:krein_smulian»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- «thm:mackey_arens»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Mackey.range_coeLM_eq_range_bilin
  - Module.dualPairing_flip_polar_polar
- «thm:predual_unique»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Ultraweak.continuousLinearEquivOfPredual
  - Predual.uniqueEquiv
- «thm:sakai_normal_iff»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Ultraweak.positive_tfae
  - Ultraweak.scottContinuous_of_scottContinuousOn_chains
- «thm:sigma_cts_of_normal_Sak_1_13_2»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Ultraweak.continuous_of_scottContinuousOn
  - Ultraweak.continuous_of_scottContinuousOn_chains
- «thm:sigma_le_s_le_tau»(Theorem)
  
  Missing tag metadata.

Structure and coverage

Informal-only11Statements with no associated Lean code yet.

Ready to formalize4Entries with an actionable next formalization step.

Formalized, ancestors open3Local Lean work is done, but prerequisite closure is still open.

Fully closed52Local code and ancestor closure are both complete.

Blocked or incomplete7Entries not covered by the highlighted readiness buckets above.

Heaviest prerequisites (55)

«thm:sigma_cts_of_normal_Sak_1_13_2»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 8statement deps: 8proof deps: 0direct uses: 1downstream unlocks: 2
Associated lean decls (2)
- Ultraweak.continuous_of_scottContinuousOn
- Ultraweak.continuous_of_scottContinuousOn_chains
«lem:zorn_base»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 7statement deps: 7proof deps: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- Ultraweak.exists_maximal_continuous_mul_right
«lem:sigma_cont_of_normal_Sak_1_7_4»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 6statement deps: 6proof deps: 0direct uses: 5downstream unlocks: 15
Associated lean decls (2)
- Ultraweak.DirectedOn.exists_isLUB
- Ultraweak.DirectedOn.isLUB_star_right_conjugate
«thm:sigma_le_s_le_tau»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 2
«lem:sigma_eq_weak_pos_on_bdd»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 16
Associated lean decls (3)
«lem:spec_masa_wstar_stonean_Sak_1_7_5»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 14
Associated lean decls (1)
- StarSubalgebra.IsMasa.extremallyDisconnected_characterSpace
«lem:star_left_mul_right_mul_sig_cts_Sak_1_7_8»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 5downstream unlocks: 11
Associated lean decls (2)
- Ultraweak.instSeparatelyContinuousMul
- Ultraweak.instIsSemitopologicalRing
«lem:wstar_unital»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 2
Associated lean decls (3)
«prop:one_sided_ideals_in_wstar_proj_Sak_1_10_1»(Proposition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 1
«thm:predual_unique»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
- Ultraweak.continuousLinearEquivOfPredual
- Predual.uniqueEquiv
Show all 45 more heaviest-prerequisite entries
- «cor:sig_clos_of_cstar_is_wstar_Sak_1_7_9»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 3
- «lem:cut_down_of_wstar»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - IsStarProjection.Corner.instCStarAlgebra
  - IsStarProjection.Corner.instPredual
- «lem:cut_down_sigma_closed_cts»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 15
  Associated lean decls (1)
  - IsStarProjection.isClosed_cornerSubmodule_of_ultraweak
- «lem:directed_sup_proj»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - Ultraweak.isStarProjection_of_isLUB
- «lem:left_mul_proj_right_mul_proj_sig_cts_Sak_1_7_7»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 12
  Associated lean decls (1)
  - Ultraweak.continuous_mul_left_of_isStarProjection
- «lem:msr_th_lemma»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Ultraweak.exists_forall_lt
- «lem:non_pos_elem_neg_for_some_state_Sak_1_7_2»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 19
  Associated lean decls (1)
  - Ultraweak.exists_positiveCLM_apply_lt_zero
- «lem:sigma_closed_star_subalg_wstar»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (2)
  - Ultraweak.predualOfIsClosed
  - Submodule.equivDualQuotientPolarSubmodule
- «prop:loc_cvx_result»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 5downstream unlocks: 12
  Associated lean decls (2)
  - Ultraweak.continuous_iff_exists_eq
  - Ultraweak.continuous_iff_mem_range
- «thm:bipolar»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 11
  Associated lean decls (2)
  - LinearMap.flip_polar_polar
  - LinearMap.IsCompatibleDual.flip_polar_polar
- «thm:krein_smulian»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 24
  Associated lean decls (3)
- «thm:mackey_arens»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - Mackey.range_coeLM_eq_range_bilin
  - Module.dualPairing_flip_polar_polar
- «thm:sakai_normal_iff»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - Ultraweak.positive_tfae
  - Ultraweak.scottContinuous_of_scottContinuousOn_chains
- «cor:spec_sa_homeo_spec_cstar»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 15
  Associated lean decls (2)
  - cfcₙ
  - IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus
- «def:sigma_top»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 17downstream unlocks: 30
  Associated lean decls (1)
  - Ultraweak
- «lem:bdd_sigma_cts_iff_bdd_s_cts_Sak_1_8_10»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
- «lem:corner_comparison»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - Ultraweak.map_le_map_of_forall_lt
  - PositiveLinearMap.le_of_le_on_isStarProjection
- «lem:dominated_sigma_cts»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Ultraweak.continuous_of_norm_sq_le
- «lem:extreme_partial_isom»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - isStarProjection_star_mul_self_of_mem_extremePoints_unitClosedBall
  - isStarProjection_self_mul_star_of_mem_extremePoints_unitClosedBall
- «lem:one_is_extreme»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - CStarAlgebra.one_mem_extremePoints_unitClosedBall
- «lem:pos_sa_sigma_closed_Sak_1_7_1»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 23
  Associated lean decls (2)
  - Ultraweak.isClosed_setOf_isSelfAdjoint
  - Ultraweak.isClosed_nonneg
- «lem:proj_sub_pos_iff_comm_eq_self»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 8
  Associated lean decls (1)
  - IsStarProjection.le_tfae
- «lem:uw_pos_sep_pts»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 18
  Associated lean decls (1)
  - Ultraweak.ext_positiveCLM
- «lem:weak_dual»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 22
  Associated lean decls (2)
  - LinearMap.IsWeak.eval_surjective
  - LinearMap.IsWeak.rightDualEquiv
- «lem:wstar_pos_approx_proj»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 13
  Associated lean decls (3)
- «prop:proj_compl_lat_wstar_Sak_1_10_2»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
- «thm:cstar_unital_iff_extreme_Sak_1_6_1»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (3)
- «cor:bipolar_submodule»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (2)
  - LinearMap.IsWeak.flip_polarSubmodule_polarSubmodule
  - LinearMap.IsCompatibleDual.flip_polarSubmodule_polarSubmodule
- «cor:nonunital_gelfand_Sak_1_2_2»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
- «cor:proj_sub_of_subproj»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - IsStarProjection.le_tfae
- «cor:sigma_eq_s_on_ball»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
- «def:Mackey_top»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (1)
  - Mackey
- «def:strong_top»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
- «def:wstar_def»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 32
  Associated lean decls (2)
  - WStarAlgebra
  - Predual
- «lem:exists_uw_ge_normal»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Ultraweak.exists_lt_of_ne_zero
- «lem:fake_approx_unit»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 5
- «lem:fin_lin_approx_of_stonean_Sak_1_3_1»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 14
  Associated lean decls (2)
  - ContinuousMap.instFiniteSpectrum
  - CStarAlgebra.FiniteSpectrum.mem_closure_hull_isStarProjection
- «lem:proj_le_one»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - IsStarProjection.le_one
- «lem:star_conj_pos»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 18
  Associated lean decls (1)
  - star_left_conjugate_nonneg
- «lem:star_pres_norm_Sak_1_1_6»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - CStarRing.to_normedStarGroup
- «lem:wstar_of_masa»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
- «prop:extr_pos_projs_Sak_1_6_2»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall
- «prop:extr_sa_sa_unitaries_Sak_1_6_3»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary
  - selfAdjoint.mem_extremePoints_unitClosedBall_iff_coe_mem_unitary
- «prop:stonean_of_cts_fcns_incr_cond_complete_Sak_1_3_2»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 15
  Associated lean decls (1)
  - ExtremallyDisconnected.ofConditionallyCompletePartialOrderSupContinuousMap
- «thm:comm_cstar_cts_fcns_Sak_1_2_1»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 23
  Associated lean decls (1)
  - gelfandStarTransform

No prerequisites (11)

«def:cstar_def»(Definition)
Associated lean decls (2)
- CStarAlgebra
- NonUnitalCStarAlgebra
«lem:selfadjoint_le_norm»(Lemma)
Associated lean decls (1)
- IsSelfAdjoint.le_algebraMap_norm_self
«thm:Banach_Alaoglu»(Theorem)
Associated lean decls (1)
- WeakDual.isCompact_closedBall
«def:weak_top»(Definition)
Associated lean decls (2)
- WeakBilin
- LinearMap.IsWeak
«lem:homeo_of_cts_bij_cpt_haus»(Lemma)
Associated lean decls (1)
- isHomeomorph_iff_continuous_bijective
«lem:cauchy_schwarz»(Lemma)
Associated lean decls (1)
- PositiveLinearMap.norm_map_star_mul_le
«thm:krein_milman»(Theorem)
Associated lean decls (2)
- IsCompact.extremePoints_nonempty
- closure_convexHull_extremePoints
«lem:pos_iff_star_mul_self_Sak_1_4_4»(Lemma)
Associated lean decls (2)
- CStarAlgebra.nonneg_TFAE
- StarOrderedRing.nonneg_iff
«def:compatible_dual»(Definition)
Associated lean decls (1)
- LinearMap.IsCompatibleDual
«lem:pos_cvx_cone»(Lemma)
Associated lean decls (1)
- ConvexCone.positive
Show all 1 more entries without prerequisites
- «lem:cts_fns_ge_zero_le_one_directed»(Lemma)

No dependents (5)

«lem:bdd_sigma_cts_iff_bdd_s_cts_Sak_1_8_10»(Lemma)
«thm:predual_unique»(Theorem)
Associated lean decls (2)
- Ultraweak.continuousLinearEquivOfPredual
- Predual.uniqueEquiv
«prop:proj_compl_lat_wstar_Sak_1_10_2»(Proposition)
«lem:wstar_of_masa»(Lemma)
«lem:cts_fns_ge_zero_le_one_directed»(Lemma)