LinearPMap

📁 Source: Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

Statistics

Metric	Count
Definitions IsFormalAdjoint, adjoint, adjointAux, adjointDomain, adjointDomainMkCLM, adjointDomainMkCLMExtend, instStar, «term_†», adjoint	9
Theorems toPMap_adjoint_eq_adjoint_toPMap_of_dense, dense_domain, isClosed, le_adjoint, adjointAux_inner, adjointAux_unique, adjointDomainMkCLMExtend_apply, adjointDomainMkCLM_apply, adjoint_apply_eq, adjoint_apply_of_dense, adjoint_apply_of_not_dense, adjoint_graph_eq_graph_adjoint, adjoint_isClosed, adjoint_isFormalAdjoint, graph_adjoint_toLinearPMap_eq_adjoint, isSelfAdjoint_def, mem_adjoint_domain_iff, mem_adjoint_domain_of_exists, mem_adjoint_iff	19
Total	28

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPMap_adjoint_eq_adjoint_toPMap_of_dense 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike	LinearPMap.adjoint LinearMap.toPMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup toLinearMap RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearIsometryEquiv CommSemiring.toSemiring Semifield.toCommSemiring starRingEnd RCLike.toStarRing RingHomInvPair.instStarRingEnd ContinuousLinearMap toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup EquivLike.toFunLike LinearIsometryEquiv.instEquivLike adjoint Top.top AddCommGroup.toAddCommMonoid Submodule.instTop	—	LinearPMap.ext RingHomInvPair.instStarRingEnd RingHomIsometric.ids smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup Submodule.ext cont RingHomCompTriple.ids IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul LinearPMap.adjoint_apply_eq adjoint_inner_left

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_domain 📖	mathematical	IsSelfAdjoint LinearPMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace LinearPMap.instStar	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike LinearPMap.domain	—	LinearPMap.isSelfAdjoint_def Submodule.eq_top_iff' RingHomCompTriple.ids Algebra.to_smulCommClass LinearPMap.mem_adjoint_domain_iff Continuous.comp SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContinuousLinearMap.cont continuous_const
isClosed 📖	mathematical	IsSelfAdjoint LinearPMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace LinearPMap.instStar	LinearPMap.IsClosed EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	LinearPMap.isSelfAdjoint_def LinearPMap.adjoint_isClosed dense_domain

LinearPMap

Definitions

Name	Category	Theorems
IsFormalAdjoint 📖	MathDef	1 math math: adjoint_isFormalAdjoint
adjoint 📖	CompOp	11 math math: adjoint_isFormalAdjoint, graph_adjoint_toLinearPMap_eq_adjoint, adjoint_apply_of_not_dense, adjoint_isClosed, ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense, IsFormalAdjoint.le_adjoint, isSelfAdjoint_def, mem_adjoint_domain_iff, mem_adjoint_domain_of_exists, adjoint_apply_of_dense, adjoint_graph_eq_graph_adjoint
adjointAux 📖	CompOp	3 math math: adjointAux_unique, adjointAux_inner, adjoint_apply_of_dense
adjointDomain 📖	CompOp	4 math math: adjointDomainMkCLM_apply, adjointDomainMkCLMExtend_apply, adjointAux_inner, adjoint_apply_of_dense
adjointDomainMkCLM 📖	CompOp	1 math math: adjointDomainMkCLM_apply
adjointDomainMkCLMExtend 📖	CompOp	1 math math: adjointDomainMkCLMExtend_apply
instStar 📖	CompOp	1 math math: isSelfAdjoint_def
«term_†» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjointAux_inner 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike domain	Inner.inner InnerProductSpace.toInner DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SetLike.instMembership adjointDomain Submodule.addCommMonoid Submodule.module LinearMap.instFunLike adjointAux toFun'	—	RingHomInvPair.instStarRingEnd RingHomIsometric.ids Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup InnerProductSpace.toDual_symm_apply adjointDomainMkCLMExtend_apply
adjointAux_unique 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike domain Inner.inner InnerProductSpace.toInner SetLike.instMembership DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid adjointDomain toFun'	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid Submodule.module LinearMap.instFunLike adjointAux	—	Dense.eq_of_inner_left adjointAux_inner
adjointDomainMkCLMExtend_apply 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike domain	DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule adjointDomainMkCLMExtend SetLike.instMembership Inner.inner InnerProductSpace.toInner adjointDomain toFun'	—	ContinuousLinearMap.extend_eq RCLike.toCompleteSpace Dense.denseRange_val IsUniformEmbedding.isUniformInducing isUniformEmbedding_subtype_val
adjointDomainMkCLM_apply 📖	mathematical	—	DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike domain instTopologicalSpaceSubtype SeminormedAddCommGroup.toPseudoMetricSpace Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule adjointDomainMkCLM Inner.inner InnerProductSpace.toInner ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid adjointDomain toFun'	—	—
adjoint_apply_eq 📖	—	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike domain Inner.inner InnerProductSpace.toInner SetLike.instMembership adjoint toFun'	—	—	adjointAux_unique adjoint_apply_of_dense
adjoint_apply_of_dense 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike domain	toFun' adjoint DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SetLike.instMembership adjointDomain Submodule.addCommMonoid Submodule.module LinearMap.instFunLike adjointAux	—	—
adjoint_apply_of_not_dense 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike domain	toFun' adjoint NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
adjoint_graph_eq_graph_adjoint 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike domain	graph adjoint Submodule.adjoint	—	Submodule.ext IsFormalAdjoint.symm adjoint_isFormalAdjoint sub_self mem_adjoint_domain_of_exists inner_conj_symm Dense.eq_of_inner_right
adjoint_isClosed 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike domain	IsClosed EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField adjoint	—	IsClosed.eq_1 adjoint_graph_eq_graph_adjoint fact_one_le_two_ennreal Submodule.adjoint.eq_1 LinearEquiv.coe_coe RingHomInvPair.ids LinearEquiv.image_eq_preimage_symm IsClosed.preimage WithLp.prod_continuous_toLp Submodule.isClosed_orthogonal
adjoint_isFormalAdjoint 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike domain	IsFormalAdjoint adjoint	—	adjointAux_inner adjoint_apply_of_dense
graph_adjoint_toLinearPMap_eq_adjoint 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike domain	Submodule.toLinearPMap Submodule.adjoint graph adjoint	—	eq_of_eq_graph adjoint_graph_eq_graph_adjoint Submodule.toLinearPMap_graph_eq Dense.eq_zero_of_inner_right inner_zero_right zero_sub
isSelfAdjoint_def 📖	mathematical	—	IsSelfAdjoint LinearPMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace instStar adjoint	—	—
mem_adjoint_domain_iff 📖	mathematical	—	Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike domain adjoint Continuous instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Submodule.module NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike LinearMap.comp SeminormedAddCommGroup.toAddCommGroup RingHomCompTriple.ids CommSemiring.toSemiring Semifield.toCommSemiring starRingEnd RCLike.toStarRing LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id innerₛₗ toFun	—	—
mem_adjoint_domain_of_exists 📖	mathematical	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike domain toFun'	adjoint	—	RingHomCompTriple.ids Algebra.to_smulCommClass mem_adjoint_domain_iff SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContinuousLinearMap.continuous

LinearPMap.IsFormalAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_adjoint 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SetLike.coe Submodule Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.setLike LinearPMap.domain LinearPMap.IsFormalAdjoint	LinearPMap LinearPMap.le LinearPMap.adjoint	—	LinearPMap.mem_adjoint_domain_of_exists symm LinearPMap.adjoint_apply_eq

Submodule

Definitions

Name	Category	Theorems
adjoint 📖	CompOp	3 math math: LinearPMap.graph_adjoint_toLinearPMap_eq_adjoint, mem_adjoint_iff, LinearPMap.adjoint_graph_eq_graph_adjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_adjoint_iff 📖	mathematical	—	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Prod.instModule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike adjoint SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal WithLp.ofLp_fst WithLp.ofLp_snd inner_neg_left

---

← Back to Index