Declaration Card Catalog

188 Declaration Cards

75 Sphere Rigidity, 69 Naimark, 11 Mankiewicz and 33 Rosenberg Cards. The Naimark Companion contains 68; the CH consequence is separate.

1. A compact-operator model for a representation

   MathlibAnnex.Analysis.CStarAlgebra.IsCompactOperatorModel

2. Maximal abelian *-subalgebras

   MathlibAnnex.Analysis.CStarAlgebra.IsMaximalAbelian

3. Pure states as real extreme points

   MathlibAnnex.Analysis.CStarAlgebra.IsPureState

4. Representations without a unit-preservation requirement

   MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation

5. Nonzero irreducibility without a unit assumption

   MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsIrreducible

6. A representative of the unique irreducible class

   MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsSingletonIrreducibleModel

7. Unitary equivalence of two representations

   MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.UnitaryEquivalent

8. The full character space is countable

   MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.countable_characterSpace_of_nonUnital_singleton

9. An isolated character away from the scalar character

   MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_isolated_character_ne_infinity

10. A projection represented by a rank-one operator

    MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_rankOne_map

11. A nonzero projection with scalar corner

    MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_scalar_corner

12. Compact operators lie in a singleton representation range

    MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_of_compact_singleton

13. Every rank-one operator has an algebra preimage

    MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_rankOne_of_singleton

14. A character becomes a joint unit eigenvector

    MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_unit_eigenvector_of_character_ne_infinity

15. A singleton model is faithful and exactly compact-valued

    MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.faithful_and_compactOperatorModel_of_singleton

16. The scalar character of the unitization

    MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.infinityCharacter

17. Faithfulness from a unique irreducible class

    MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.injective_of_singleton

18. Every operator in a singleton image is compact

    MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.isCompactOperator_map_of_singleton

19. Singleton condition tested against all irreducible representations

    MathlibAnnex.Analysis.CStarAlgebra.Representation.IsSingletonIrreducibleModelAmongNonUnital

20. Compact-operator conclusion for the unital singleton condition

    MathlibAnnex.Analysis.CStarAlgebra.Representation.faithful_and_compactOperatorModel_of_singleton_amongNonUnital

21. Finite-dimensional algebra in the unital singleton case

    MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_algebra_of_singleton_amongNonUnital

22. A unital singleton model acts in finite dimension

    MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_space_of_singleton

23. Finite-dimensional representation space in the unital singleton case

    MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_space_of_singleton_amongNonUnital

24. A faithful singleton model forces simplicity

    MathlibAnnex.Analysis.CStarAlgebra.Representation.isSimpleCStarAlgebra_of_singleton_of_injective

25. An infinite-dimensional unital algebra has no separable singleton model

    MathlibAnnex.Analysis.CStarAlgebra.Representation.not_singleton_amongNonUnital_of_infiniteDimensional

26. Full operator image in finite dimension

    MathlibAnnex.Analysis.CStarAlgebra.Representation.surjective_of_irreducible_of_finiteDimensional

27. A character separating a closed ideal

    MathlibAnnex.Analysis.CStarAlgebra.exists_character_annihilating_closedIdeal_of_not_mem

28. A maximal abelian subalgebra containing a self-adjoint element

    MathlibAnnex.Analysis.CStarAlgebra.exists_maximalAbelian_containing_isSelfAdjoint

29. A character extends to a pure state

    MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_extension

30. A pure state detects a nonzero square

    MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_nonzero_on_star_mul_self

31. The GNS representation of a pure state is irreducible

    MathlibAnnex.Analysis.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom

32. Inverse maps on open sets with global metric bounds

    MathlibAnnex.BilipschitzOrientation.BiLipschitzOpenData

33. A positive lower metric bound passes to the derivative

    MathlibAnnex.BilipschitzOrientation.fderiv_lower_bound

34. The signed Jacobian integral is a sign times target volume

    MathlibAnnex.BilipschitzOrientation.integral_det_fderiv_eq_signed_volume

35. Signed transfer from the absolute Jacobian formula

    MathlibAnnex.BilipschitzOrientation.signed_area_transfer

36. Almost-everywhere constancy of the sign on a preconnected target

    MathlibAnnex.BilipschitzOrientation.targetJacobianSign_ae_const

37. The transported Jacobian sign has zero weak gradient

    MathlibAnnex.BilipschitzOrientation.weakDivergenceZero_targetJacobianSign

38. Weak Piola identity for a compactly supported test field

    MathlibAnnex.BilipschitzOrientation.weak_piola

39. The closed operator algebra generated by a representation and extra operators

    MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget

40. An irreducible operator algebra constructed from projection shells

    MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_atomicShellModel

41. The atomic-shell construction on selected pure-GNS fibers

    MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_pureAtomicShellModel

42. The C*-algebra generated by the CAR representation and the shell unitaries

    MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleAlgebra

43. A two-sided inner intertwining sequence for two states

    MathlibAnnex.CStarAlgebra.CAR.HasInnerIntertwiningSequence

44. The CAR algebra as a completion of finite matrix stages

    MathlibAnnex.CStarAlgebra.CAR.Limit

45. Approximately inner homogeneity of pure CAR states

    MathlibAnnex.CStarAlgebra.CAR.PureStateHomogeneity

46. A fixed representative family of CAR shell data

    MathlibAnnex.CStarAlgebra.CAR.RepresentativeShellFamily

47. Every irreducible representation is unitarily equivalent to the inclusion

    MathlibAnnex.CStarAlgebra.CAR.ambientInclusion_unitaryEquivalent

48. A simple C*-algebra with a unique irreducible representation class

    MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint

49. A separably represented C*-algebra with no separable irreducible representation

    MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation

50. The ambient representation of the fixed algebra

    MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleRepresentation

51. CH and a Naimark counterexample of norm density aleph one

    MathlibAnnex.CStarAlgebra.CAR.continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity

52. Normalization and the trace identity determine the CAR trace

    MathlibAnnex.CStarAlgebra.CAR.eq_trace_of_apply_one_of_mul_comm

53. An irreducible CAR representation has no nonzero compact image

    MathlibAnnex.CStarAlgebra.CAR.eq_zero_of_isCompactOperator_image

54. A Naimark counterexample of continuum norm density

    MathlibAnnex.CStarAlgebra.CAR.existsNaimarkCounterexampleOfDensity_continuum

55. Uniqueness among all state extensions of the CAR trace

    MathlibAnnex.CStarAlgebra.CAR.existsUnique_state_extension_trace

56. The fixed shell target has a unique tracial state

    MathlibAnnex.CStarAlgebra.CAR.existsUnique_tracial_state

57. Realizing a shell family by a faithful irreducible operator algebra

    MathlibAnnex.CStarAlgebra.CAR.exists_completedAtomicShellModel

58. Lifting a corner involution to an ambient CAR unitary

    MathlibAnnex.CStarAlgebra.CAR.exists_liftedCornerExponential_apply_eq_involution

59. An irreducible target representation has a surviving fixed space

    MathlibAnnex.CStarAlgebra.CAR.exists_nonzero_targetFixedSpace

60. Pointed unitary transport between trace-cyclic target representations

    MathlibAnnex.CStarAlgebra.CAR.exists_pointed_unitary_of_trace_of_cyclic

61. Realizing a finite Gram matrix in a represented CAR corner

    MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerFamily_with_gram

62. Assembling selected GNS cyclic subspaces into an isometric source representation

    MathlibAnnex.CStarAlgebra.CAR.exists_selectedAtomicCyclicIsometry

63. Cross-representation state approximation with a protected finite set

    MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_crossRepresentation_path_approx

64. Exact vector transport along an almost central unitary path

    MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt

65. Extending the CAR trace to the fixed shell target

    MathlibAnnex.CStarAlgebra.CAR.exists_state_extension_trace

66. The cyclic sum fills every irreducible target representation

    MathlibAnnex.CStarAlgebra.CAR.exists_surjective_selectedAtomicCyclicIsometry

67. A common root vector realizes every selected state through the generators

    MathlibAnnex.CStarAlgebra.CAR.exists_targetDefectVectorFamily

68. Reconstructing a represented unitary from its shells and residual corner

    MathlibAnnex.CStarAlgebra.CAR.exists_targetShellReconstruction

69. Purifying a vector state on a finite CAR stage

    MathlibAnnex.CStarAlgebra.CAR.exists_unitVector_vectorFunctional_eq_on_stage

70. Approximating another vector state along a unitary path

    MathlibAnnex.CStarAlgebra.CAR.exists_unitary_crossRepresentation_path_approx

71. Exact norm density of the fixed atomic algebra

    MathlibAnnex.CStarAlgebra.CAR.hasDensityCharacter_atomicCounterexampleAlgebra

72. Pure CAR states admit two-sided inner intertwining sequences

    MathlibAnnex.CStarAlgebra.CAR.hasInnerIntertwiningSequence_of_pure

73. Pure-state homogeneity of the completed CAR algebra

    MathlibAnnex.CStarAlgebra.CAR.homogeneity

74. Choosing the CAR shell family from proved homogeneity

    MathlibAnnex.CStarAlgebra.CAR.homogeneityShellFamily

75. Two-sided inner sequences imply pure-state homogeneity

    MathlibAnnex.CStarAlgebra.CAR.homogeneity_of_innerIntertwiningSequences

76. The atomic common range is one embedded GNS line

    MathlibAnnex.CStarAlgebra.CAR.iInf_range_atomic_transportedFlag_eq_span

77. Purity of the completed root state

    MathlibAnnex.CStarAlgebra.CAR.isPureState_rootState

78. Simplicity of the completed CAR algebra

    MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_limit

79. Closed-ideal simplicity of the shell-generated algebra

    MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_shellFamilyTarget

80. The completed CAR algebra is infinite-dimensional

    MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional

81. The shell-generated algebra is not an algebra of all compact operators

    MathlibAnnex.CStarAlgebra.CAR.not_isCompactOperatorModel_shellFamilyTarget

82. No nonzero irreducible representation on a separable Hilbert space

    MathlibAnnex.CStarAlgebra.CAR.not_isIrreducible_of_separable

83. A finite-row average centralizes its matrix stage

    MathlibAnnex.CStarAlgebra.CAR.ofStage_commute_rowAverage

84. The decreasing root projections in the CAR completion

    MathlibAnnex.CStarAlgebra.CAR.rootFlag

85. The product-vector state on the completed CAR algebra

    MathlibAnnex.CStarAlgebra.CAR.rootState

86. The atomic direct sum of the selected CAR representations

    MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation

87. The matching GNS fiber retains exactly its cyclic line

    MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_rankOne

88. An inequivalent GNS fiber has no residual common range

    MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_zero

89. The fixed algebra on the CAR trace Hilbert space

    MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation

90. Faithfulness of the representation on the CAR trace Hilbert space

    MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation_injective

91. Structural properties of one shell-generated C*-algebra

    MathlibAnnex.CStarAlgebra.CAR.shellFamilyEndpoint

92. The ambient inclusion of the fixed shell-family target

    MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion

93. Unitary equivalence without an initial unitality assumption

    MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion_unitaryEquivalent_nonUnital

94. The CAR source map into the fixed shell-family target

    MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom

95. The normalized trace on a finite CAR stage

    MathlibAnnex.CStarAlgebra.CAR.stageTrace

96. Root compression becomes scalar in norm

    MathlibAnnex.CStarAlgebra.CAR.tendsto_norm_compressionError

97. Transported flags vanish on vectors generated by a trace vector

    MathlibAnnex.CStarAlgebra.CAR.tendsto_transportedFlag_orbit_zero

98. Constructing the normalized trace on the completed CAR algebra

    MathlibAnnex.CStarAlgebra.CAR.trace

99. The unique trace extension is tracial on the whole target

    MathlibAnnex.CStarAlgebra.CAR.traceExtension_mul_comm

100. The target represented on the CAR trace GNS space

     MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation

101. Faithfulness of the representation on the CAR trace Hilbert space

     MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation_injective

102. Shell matching fixes the trace of transported flags

     MathlibAnnex.CStarAlgebra.CAR.trace_transportedFlag

103. The GNS representation of the target trace extension

     MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation

104. Faithfulness of the target-state GNS representation

     MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation_injective

105. Distinct GNS classes have no unitary intertwiner

     MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation

106. The selected GNS representation of a pure-state class

     MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation

107. The preimage ideal of the compact operators

     MathlibAnnex.CStarAlgebra.compactPreimageIdeal

108. Exact projection links for one approximately inner automorphism

     MathlibAnnex.CStarAlgebra.exists_shell_family_of_approximately_inner

109. A determinant difference bound in the sup operator norm

     MathlibAnnex.ContinuousLinearMap.abs_det_sub_le_max

110. Positivity of the determinant maximum

     MathlibAnnex.DeterminantFrame.determinantMaximum_pos

111. An attained absolute determinant maximum

     MathlibAnnex.DeterminantFrame.exists_maximizingFrame

112. A common inverse estimate from row Cramer

     MathlibAnnex.DeterminantFrame.inverseBoundConstant_bound

113. The set of near-maximal dual frames

     MathlibAnnex.DeterminantFrame.nearMaxFrames

114. A seminorm with two-sided bounds against a reference norm

     MathlibAnnex.EquivalentSeminorm

115. Continuous linear maps bounded by a seminorm

     MathlibAnnex.EquivalentSeminorm.IsContraction

116. All Plücker bodies determine the norm up to linear isometry

     MathlibAnnex.EquivalentSeminorm.nonempty_linearIsometryEquiv_of_pluckerBodies_eq

117. A seminorm increment bound passes to every derivative direction

     MathlibAnnex.FDeriv.norm_apply_le_seminorm_of_lipschitz

118. Equal Plücker bodies yield matching generators with an almost-isometric representative

     MathlibAnnex.FiniteRecovery.nonempty_almostIsometryMatch_of_all_body_eq

119. The chosen support slice consists of almost-isometric generators

     MathlibAnnex.FiniteRecovery.targetRawSupportMaximizer_good

120. A strict lower bound on a norm's unit sphere

     MathlibAnnex.FiniteSup.FinMapAlmostIsometric

121. Mankiewicz extension on open connected domains

     MathlibAnnex.IsometryEquiv.existsUnique_affineExtension

122. Affine extension from open balls

     MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_ball

123. Affine extension from equal-radius closed balls

     MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_closedBall

124. Convex-set extension via ambient interiors

     MathlibAnnex.IsometryEquiv.existsUnique_affineExtension_of_convex

125. Local affine-isometry chart on a smaller ball

     MathlibAnnex.IsometryEquiv.exists_affineExtension_eqOn_ball

126. Center transport under bounded point-reflection symmetry

     MathlibAnnex.IsometryEquiv.map_center_of_mapsTo_pointReflection

127. Affine-segment preservation on a quarter ball

     MathlibAnnex.IsometryEquiv.map_lineMap_of_mem_ball

128. Midpoint preservation on a quarter ball

     MathlibAnnex.IsometryEquiv.map_midpoint_of_mem_ball

129. Midpoint preservation on a symmetric lens

     MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens

130. Midpoint preservation under lens containment

     MathlibAnnex.IsometryEquiv.map_midpoint_of_symmetricLens_subset

131. Maximal minors scaled by the reference ball volume

     MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors

132. Cramer’s rule for coordinates of a row

     MathlibAnnex.Matrix.det_smul_vecMul_nonsingInv_eq_updateRowDet

133. A unique right factor from proportional oriented maximal minors

     MathlibAnnex.Matrix.existsUnique_factor_of_orientedMaximalMinorsProportional

134. The family of maximal minors in increasing row order

     MathlibAnnex.Matrix.maximalMinors

135. Right multiplication scales every maximal minor by one determinant

     MathlibAnnex.Matrix.maximalMinors_mul

136. Determinant integrals under strong Lⁿ convergence

     MathlibAnnex.MeasureTheory.tendsto_integral_det_of_strongLn

137. Mollification by a normalized smooth kernel

     MathlibAnnex.Mollification.mollify

138. Strong local convergence of mollified derivatives

     MathlibAnnex.Mollification.tendsto_eLpNorm_fderiv_mollify_sub

139. Boundary agreement determines maximal-minor integrals

     MathlibAnnex.NullLagrangian.integral_maximalMinor_eq_of_pointwise_boundary_eq

140. Maximal-minor integral differences for Lipschitz perturbations

     MathlibAnnex.NullLagrangian.integral_maximalMinor_fderiv_add_sub_eq_zero_of_lipschitzWith

141. A cofactor row by row replacement

     MathlibAnnex.Piola.cofactorRow

142. The divergence-free cofactor identity

     MathlibAnnex.Piola.divergence_cofactorRowField_eq_zero

143. A component flux gives a determinant difference

     MathlibAnnex.Piola.divergence_componentFlux_eq_det_sub

144. Zero integral of a compactly supported divergence

     MathlibAnnex.Piola.integral_coordinateDivergence_eq_zero_of_contDiff_hasCompactSupport

145. Smooth compact perturbations preserve the determinant integral difference

     MathlibAnnex.Piola.integral_det_fderiv_add_sub_eq_zero_of_contDiff

146. The set average of derivative generators

     MathlibAnnex.Plucker.derivativeAverage

147. A common orientation sign for the radial derivative average

     MathlibAnnex.Plucker.derivativeAverage_comp_linear_radial

148. The average of contractive derivative generators lies in the body

     MathlibAnnex.Plucker.derivativeAverage_mem_body

149. One boundary extension with all five analytic properties

     MathlibAnnex.Plucker.exists_extension_with_derivativeAverage_mem

150. The symmetric convex body of contraction minors

     MathlibAnnex.PluckerBody.body

151. Sphere isometries preserve the Plücker body

     MathlibAnnex.PluckerBody.eq_of_sphereIsometry

152. Compactness of the signed generator set

     MathlibAnnex.PluckerBody.isCompact_generators

153. A target contraction generator lies in the source body

     MathlibAnnex.PluckerBody.normalizedGenerator_mem_of_sphereIsometry

154. The recovered contraction maps one unit ball onto the other

     MathlibAnnex.PluckerRecovery.LimitCertificate.image_unitBall_eq

155. A volume-normalized linear contraction obtained by a limit

     MathlibAnnex.PluckerRecovery.nonempty_limitCertificate_of_pluckerBodies_eq

156. Almost-contractive linear recovery with exact volume scaling

     MathlibAnnex.PluckerRecovery.nonempty_linearCertificate_of_pluckerBodies_eq

157. The satellite polynomial is linear in the maximal-minor vector

     MathlibAnnex.PluckerSupport.pluckerPairing_satelliteCoefficients_maximalMinors

158. A nearby norming point gives an almost-norming evaluation

     MathlibAnnex.Satellite.abs_eval_lower_of_norms_nearby

159. Absolute maximization forces a near-maximal base

     MathlibAnnex.Satellite.absoluteMaximizer_base_nearMax

160. Each satellite norms its coefficient preimage in absolute value

     MathlibAnnex.Satellite.absoluteMaximizer_satellite_norms_preimage

161. One fixed satellite family almost norms every detected unit vector

     MathlibAnnex.Satellite.absoluteMaximizer_satellites_almost_norm

162. A finite absolute-maximizing family almost norms the unit sphere

     MathlibAnnex.Satellite.exists_goodSatellitePackage

163. A weighted determinant polynomial with satellites

     MathlibAnnex.Satellite.satellitePolynomial

164. Equality of seminorm balls under a linear bijection preserves the seminorms

     MathlibAnnex.SeminormBall.map_eq

165. A compact proper subset of a seminorm ball has smaller Haar measure

     MathlibAnnex.SeminormBall.measure_lt

166. Finite-dimensionality transfers across a sphere isometry

     MathlibAnnex.Sphere.finiteDimensional_codomain

167. Isometric unit spheres force equal finite dimensions

     MathlibAnnex.Sphere.finrank_eq

168. The radial extension is 3-Lipschitz

     MathlibAnnex.Sphere.lipschitzWith_radialExtension

169. The unit-sphere chord metric determines the ambient normed space

     MathlibAnnex.Sphere.nonempty_isometryEquiv_iff_nonempty_linearIsometryEquiv_of_finiteDimensional

170. Radial extension of an isometry between unit spheres

     MathlibAnnex.Sphere.radialExtension

171. The absolute Jacobian integral of a radial sphere extension

     MathlibAnnex.Sphere.radialExtension_integral_abs_det

172. The inverse sphere isometry gives the inverse radial map

     MathlibAnnex.Sphere.radialExtension_leftInverse

173. An isolated point in a countable Baire space

     MathlibAnnex.Topology.exists_isOpen_singleton

174. Vanishing weak gradient tested by divergence

     MathlibAnnex.WeakDivergenceZero

175. Global almost-everywhere constancy on a preconnected domain

     MathlibAnnex.WeakDivergenceZero.exists_aeConstantOn

176. A continuous function with zero weak gradient is constant

     MathlibAnnex.WeakDivergenceZero.exists_eqOn

177. Local almost-everywhere constancy from the weak equation

     MathlibAnnex.WeakDivergenceZero.nonempty_localAEConstantAt

178. Differentiating a local mollification through its kernel

     MathlibAnnex.WeakGradient.localMollification_fderiv_apply

179. Zero weak gradient gives zero derivatives of local mollifications

     MathlibAnnex.WeakGradient.localMollification_fderiv_apply_eq_zero

180. Gluing one almost-everywhere constant over a countable cover

     MathlibAnnex.aeConstantOn_of_countableCover

181. Identifying constants on an open overlap

     MathlibAnnex.aeConstants_eq_of_open_overlap

182. A support face is the convex hull of the maximizing generators

     MathlibAnnex.convexHull_maxSlice_eq_supportFace

183. Divergence as the trace of a derivative

     MathlibAnnex.divergence

184. From local to global almost-everywhere constancy

     MathlibAnnex.exists_aeConstantOn_of_local

185. A common generator selected from equal convex hulls

     MathlibAnnex.exists_common_of_convexHull_eq

186. The convex hull of a compact set in a finite real coordinate space

     MathlibAnnex.isCompact_convexHull_pi

187. Successive maximum refinement by an ordered list of functionals

     MathlibAnnex.lexicographicRefine

188. Symmetric lens

     MathlibAnnex.symmetricLens

Version history