LinearPMap

📁 Source: Mathlib/Topology/Algebra/Module/LinearPMap.lean

Statistics

Metric	Count
Definitions LinearPMap, HasCore, IsClosable, IsClosed, closure	5
Theorems closure_eq, le_domain, closureIsClosable, closure_isClosed, closure_mono, existsUnique, graph_closure_eq_closure_graph, leIsClosable, isClosable, closureHasCore, closure_def, closure_def', closure_inverse_graph, hasCore_def, inverse_closed_iff, inverse_closure, inverse_isClosable_iff, isClosable_iff_exists_closed_extension, le_closure	19
Total	24

LinearPMap

Definitions

Name	Category	Theorems
HasCore 📖	CompData	1 math math: closureHasCore
IsClosable 📖	MathDef	2 math math: IsClosed.isClosable, isClosable_iff_exists_closed_extension
IsClosed 📖	MathDef	5 math math: IsSelfAdjoint.isClosed, adjoint_isClosed, IsClosable.closure_isClosed, inverse_closed_iff, isClosable_iff_exists_closed_extension
closure 📖	CompOp	11 math math: IsClosable.closure_mono, closureHasCore, hasCore_def, HasCore.closure_eq, inverse_isClosable_iff, closure_def', IsClosable.closure_isClosed, closure_def, le_closure, IsClosable.closureIsClosable, IsClosable.graph_closure_eq_closure_graph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closureHasCore 📖	mathematical	—	HasCore closure domain CommRing.toRing	—	le_closure ext Submodule.ext domRestrict_apply
closure_def 📖	mathematical	IsClosable	closure LinearPMap CommRing.toRing Submodule Ring.toSemiring Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule Submodule.topologicalClosure instTopologicalSpaceProd graph	—	—
closure_def' 📖	mathematical	IsClosable	closure	—	—
closure_inverse_graph 📖	mathematical	LinearMap.ker Submodule Ring.toSemiring CommRing.toRing AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike domain Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring toFun Bot.bot Submodule.instBot IsClosable closure	graph inverse Submodule.topologicalClosure instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule Prod.continuousConstSMul SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction ContinuousSMul.continuousConstSMul Prod.continuousAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	Prod.continuousConstSMul ContinuousSMul.continuousConstSMul Prod.continuousAdd RingHomSurjective.ids RingHomInvPair.ids inverse_graph IsClosable.graph_closure_eq_closure_graph SetLike.ext' Set.image_congr HasSubset.Subset.antisymm Set.instAntisymmSubset image_closure_subset_closure_image continuous_swap Equiv.image_eq_preimage_symm Continuous.closure_preimage_subset
hasCore_def 📖	mathematical	HasCore	closure domRestrict CommRing.toRing	—	HasCore.closure_eq
inverse_closed_iff 📖	mathematical	LinearMap.ker Submodule Ring.toSemiring CommRing.toRing AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike domain Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring toFun Bot.bot Submodule.instBot	IsClosed inverse	—	IsClosed.eq_1 RingHomSurjective.ids RingHomInvPair.ids inverse_graph ContinuousLinearEquiv.isClosed_image
inverse_closure 📖	mathematical	LinearMap.ker Submodule Ring.toSemiring CommRing.toRing AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike domain Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring toFun Bot.bot Submodule.instBot IsClosable closure	inverse	—	eq_of_eq_graph Prod.continuousConstSMul ContinuousSMul.continuousConstSMul Prod.continuousAdd closure_inverse_graph IsClosable.graph_closure_eq_closure_graph inverse_isClosable_iff
inverse_isClosable_iff 📖	mathematical	LinearMap.ker Submodule Ring.toSemiring CommRing.toRing AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike domain Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring toFun Bot.bot Submodule.instBot IsClosable	inverse closure	—	LinearMap.ker_eq_bot' RingHomSurjective.ids RingHomInvPair.ids inverse_graph image_closure_subset_closure_image continuous_swap Prod.continuousConstSMul ContinuousSMul.continuousConstSMul Prod.continuousAdd Submodule.topologicalClosure_coe SetLike.mem_coe IsClosable.graph_closure_eq_closure_graph image_iff toFun_eq_coe graph_fst_eq_zero_snd closure_inverse_graph
isClosable_iff_exists_closed_extension 📖	mathematical	—	IsClosable IsClosed LinearPMap CommRing.toRing le	—	IsClosable.closure_isClosed le_closure IsClosable.leIsClosable IsClosed.isClosable
le_closure 📖	mathematical	—	LinearPMap CommRing.toRing le closure	—	le_of_le_graph Prod.continuousConstSMul ContinuousSMul.continuousConstSMul Prod.continuousAdd IsClosable.graph_closure_eq_closure_graph Submodule.le_topologicalClosure closure_def' le_refl

LinearPMap.HasCore

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_eq 📖	mathematical	LinearPMap.HasCore	LinearPMap.closure LinearPMap.domRestrict CommRing.toRing	—	—
le_domain 📖	mathematical	LinearPMap.HasCore	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearPMap.domain CommRing.toRing	—	—

LinearPMap.IsClosable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closureIsClosable 📖	mathematical	LinearPMap.IsClosable	LinearPMap.closure	—	LinearPMap.IsClosed.isClosable closure_isClosed
closure_isClosed 📖	mathematical	LinearPMap.IsClosable	LinearPMap.IsClosed LinearPMap.closure	—	LinearPMap.IsClosed.eq_1 Prod.continuousConstSMul ContinuousSMul.continuousConstSMul Prod.continuousAdd graph_closure_eq_closure_graph Submodule.isClosed_topologicalClosure
closure_mono 📖	mathematical	LinearPMap.IsClosable LinearPMap CommRing.toRing LinearPMap.le	LinearPMap.closure	—	LinearPMap.le_of_le_graph Prod.continuousConstSMul ContinuousSMul.continuousConstSMul Prod.continuousAdd graph_closure_eq_closure_graph leIsClosable Submodule.topologicalClosure_mono LinearPMap.le_graph_of_le
existsUnique 📖	mathematical	LinearPMap.IsClosable	ExistsUnique LinearPMap CommRing.toRing Submodule Ring.toSemiring Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule Submodule.topologicalClosure instTopologicalSpaceProd Prod.continuousConstSMul SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction ContinuousSMul.continuousConstSMul Prod.continuousAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup LinearPMap.graph	—	existsUnique_of_exists_of_unique Prod.continuousConstSMul ContinuousSMul.continuousConstSMul Prod.continuousAdd LinearPMap.eq_of_eq_graph
graph_closure_eq_closure_graph 📖	mathematical	LinearPMap.IsClosable	Submodule.topologicalClosure Ring.toSemiring CommRing.toRing instTopologicalSpaceProd Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule Prod.continuousConstSMul SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction ContinuousSMul.continuousConstSMul Prod.continuousAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup LinearPMap.graph LinearPMap.closure	—	Prod.continuousConstSMul ContinuousSMul.continuousConstSMul Prod.continuousAdd LinearPMap.closure_def
leIsClosable 📖	—	LinearPMap.IsClosable LinearPMap CommRing.toRing LinearPMap.le	—	—	Prod.continuousConstSMul ContinuousSMul.continuousConstSMul Prod.continuousAdd Submodule.topologicalClosure_mono LinearPMap.le_graph_of_le Submodule.toLinearPMap_graph_eq LinearPMap.graph_fst_eq_zero_snd

LinearPMap.IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosable 📖	mathematical	—	LinearPMap.IsClosable	—	IsClosed.submodule_topologicalClosure_eq Prod.continuousConstSMul ContinuousSMul.continuousConstSMul Prod.continuousAdd

(root)

Definitions

Name	Category	Theorems
LinearPMap 📖	CompData	45 math math: HahnEmbedding.IsPartial.baseEmbedding_le, LinearPMap.zero_domain, LinearPMap.left_le_sup, Module.Baer.chain_linearPMap_of_chain_extensionOf, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, LinearPMap.neg_graph, LinearPMap.neg_apply, LinearPMap.sub_domain, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, LinearPMap.instIsScalarTower, LinearPMap.le_graph_iff, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, LinearPMap.smul_domain, HahnEmbedding.Partial.orderTop_eq_iff, LinearPMap.le_of_le_graph, RieszExtension.exists_top, LinearPMap.sub_apply, LinearPMap.coe_smul, LinearPMap.IsFormalAdjoint.le_adjoint, LinearPMap.add_apply, LinearPMap.isSelfAdjoint_def, LinearPMap.right_le_sup, RieszExtension.step, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, HahnEmbedding.Partial.mem_domain, LinearPMap.closure_def, LinearPMap.smul_graph, LinearPMap.neg_domain, LinearPMap.vadd_apply, LinearPMap.vadd_domain, LinearPMap.isClosable_iff_exists_closed_extension, LinearPMap.le_closure, LinearPMap.smul_apply, LinearPMap.instSMulCommClass, LinearPMap.coe_vadd, LinearPMap.domRestrict_le, HahnEmbedding.Partial.exists_domain_eq_top, HahnEmbedding.Partial.exists_isMax, Module.Baer.ExtensionOf.toLinearPMap_injective, LinearPMap.add_domain, LinearPMap.domain_mono, LinearPMap.zero_apply, LinearPMap.IsClosable.existsUnique, LinearPMap.le_of_eqLocus_ge, HahnEmbedding.Partial.toOrderAddMonoidHom_injective

---

← Back to Index