ClosedSubmodule

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

Statistics

Metric	Count
Definitions `ClosedSubmodule`, `comap`, `instCoeSubmodule`, `instCompleteLatticeOfT1Space`, `instCompleteSemilatticeInf`, `instCompleteSemilatticeSup`, `instInf`, `instInfSet`, `instLattice`, `instMax`, `instOrderBot`, `instOrderTop`, `instPartialOrder`, `instSemilatticeInf`, `instSemilatticeSup`, `instSetLike`, `instSupSet`, `map`, `mapEquiv`, `toCloseds`, `toSubmodule`, `closure`	22
Theorems `carrier_eq_coe`, `closure_map_eq_mapEquiv_closure`, `closure_toSubmodule_eq`, `coe_bot`, `coe_comap`, `coe_iInf`, `coe_iSup`, `coe_inf`, `coe_sInf`, `coe_sSup`, `coe_sup`, `coe_toCloseds`, `coe_toSubmodule`, `coe_top`, `comap_comap`, `comap_id`, `ext`, `ext_iff`, `gc_map_comap`, `instAddSubmonoidClass`, `instCanLiftSubmoduleToSubmoduleIsClosedCoe`, `instSMulMemClass`, `isClosed`, `isClosed'`, `mapEquiv_apply`, `mapEquiv_bot_eq_bot`, `mapEquiv_inf_eq`, `mapEquiv_sup_eq`, `mapEquiv_symm`, `mapEquiv_top_eq_top`, `map_id`, `map_le_iff_le_comap`, `mem_bot`, `mem_comap`, `mem_iInf`, `mem_iSup`, `mem_inf`, `mem_mapEquiv_iff`, `mem_mapEquiv_iff'`, `mem_mk`, `mem_sInf`, `mem_sSup`, `mem_sup`, `mem_toSubmodule_iff`, `mem_top`, `toCloseds_injective`, `toSubmodule_bot`, `toSubmodule_comap`, `toSubmodule_iInf`, `toSubmodule_iSup`, `toSubmodule_inf`, `toSubmodule_injective`, `toSubmodule_le_toSubmodule`, `toSubmodule_sInf`, `toSubmodule_sSup`, `toSubmodule_sup`, `toSubmodule_top`, `closure_eq`, `closure_eq'`, `closure_le`, `coe_closure`, `mem_closure_iff`, `instCompleteSpaceSubtypeMemClosedSubmodule`	63
Total	85

ClosedSubmodule

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	7 math math: `comap_comap`, `mem_comap`, `comap_id`, `gc_map_comap`, `toSubmodule_comap`, `map_le_iff_le_comap`, `coe_comap`
`instCoeSubmodule` 📖	CompOp	—
`instCompleteLatticeOfT1Space` 📖	CompOp	—
`instCompleteSemilatticeInf` 📖	CompOp	—
`instCompleteSemilatticeSup` 📖	CompOp	—
`instInf` 📖	CompOp	15 math math: `ProperCone.dual_insert`, `inf_orthogonal`, `StandardSubspace.IsSeparating`, `mem_inf`, `sup_orthogonal`, `ProperCone.innerDual_union`, `mulI_inf`, `ProperCone.innerDual_insert`, `coe_inf`, `inf_orthogonal_eq_bot`, `toSubmodule_inf`, `ProperCone.dual_union`, `symplComp_sup`, `symplComp_inf`, `mapEquiv_inf_eq`
`instInfSet` 📖	CompOp	12 math math: `ProperCone.dual_sUnion`, `mem_iInf`, `ProperCone.innerDual_sUnion`, `coe_sInf`, `ProperCone.dual_iUnion`, `toSubmodule_iInf`, `iInf_orthogonal`, `coe_iInf`, `mem_sInf`, `sInf_orthogonal`, `ProperCone.innerDual_iUnion`, `toSubmodule_sInf`
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	10 math math: `mapEquiv_sup_eq`, `toSubmodule_sup`, `inf_orthogonal`, `mulI_sup`, `StandardSubspace.IsCyclic`, `sup_orthogonal`, `mem_sup`, `symplComp_sup`, `coe_sup`, `symplComp_inf`
`instOrderBot` 📖	CompOp	15 math math: `ProperCone.innerDual_univ`, `ProperCone.coe_bot`, `mem_bot`, `mapEquiv_bot_eq_bot`, `bot_orthogonal_eq_top`, `StandardSubspace.IsSeparating`, `top_orthogonal_eq_bot`, `ProperCone.dual_univ`, `coe_bot`, `orthogonal_eq_top_iff`, `ProperCone.toPointedCone_bot`, `inf_orthogonal_eq_bot`, `ProperCone.mem_bot`, `toSubmodule_bot`, `orthogonal_disjoint`
`instOrderTop` 📖	CompOp	12 math math: `mapEquiv_top_eq_top`, `ProperCone.innerDual_zero`, `bot_orthogonal_eq_top`, `top_orthogonal_eq_bot`, `StandardSubspace.IsCyclic`, `ProperCone.dual_zero`, `orthogonal_eq_top_iff`, `ProperCone.innerDual_empty`, `mem_top`, `ProperCone.dual_empty`, `coe_top`, `toSubmodule_top`
`instPartialOrder` 📖	CompOp	31 math math: `mapEquiv_top_eq_top`, `ProperCone.innerDual_univ`, `orthogonal_gc`, `ProperCone.coe_bot`, `mem_bot`, `mapEquiv_bot_eq_bot`, `ProperCone.innerDual_zero`, `orthogonal_le`, `bot_orthogonal_eq_top`, `StandardSubspace.IsSeparating`, `top_orthogonal_eq_bot`, `ProperCone.dual_univ`, `StandardSubspace.IsCyclic`, `coe_bot`, `orthogonal_orthogonal_monotone`, `Submodule.closure_le`, `ProperCone.dual_zero`, `gc_map_comap`, `orthogonal_eq_top_iff`, `toSubmodule_le_toSubmodule`, `ProperCone.toPointedCone_bot`, `inf_orthogonal_eq_bot`, `ProperCone.innerDual_empty`, `map_le_iff_le_comap`, `mem_top`, `ProperCone.mem_bot`, `toSubmodule_bot`, `ProperCone.dual_empty`, `coe_top`, `orthogonal_disjoint`, `toSubmodule_top`
`instSemilatticeInf` 📖	CompOp	—
`instSemilatticeSup` 📖	CompOp	—
`instSetLike` 📖	CompOp	41 math math: `sub_mem_orthogonal_of_inner_right`, `mem_iff`, `mem_comap`, `ProperCone.coe_positive`, `mem_orthogonal'`, `coe_sSup`, `mem_iInf`, `instSMulMemClass`, `mem_bot`, `mem_toSubmodule_iff`, `coe_sInf`, `mem_mapEquiv_iff'`, `orthogonal_eq_inter`, `coe_bot`, `mem_inf`, `mem_symplComp_iff`, `coe_toCloseds`, `sub_mem_orthogonal_of_inner_left`, `mem_orthogonal`, `mem_orthogonal_toSubmodule_iff`, `mem_sup`, `mem_iSup`, `mem_orthogonal_iff`, `coe_inf`, `coe_iInf`, `isClosed`, `mem_sSup`, `mem_sInf`, `mem_mk`, `mem_top`, `Submodule.coe_closure`, `mem_mapEquiv_iff`, `coe_top`, `coe_iSup`, `coe_sup`, `instCompleteSpaceSubtypeMemClosedSubmodule`, `coe_comap`, `carrier_eq_coe`, `coe_toSubmodule`, `instAddSubmonoidClass`, `Submodule.mem_closure_iff`
`instSupSet` 📖	CompOp	8 math math: `coe_sSup`, `toSubmodule_iSup`, `iInf_orthogonal`, `mem_iSup`, `toSubmodule_sSup`, `mem_sSup`, `sInf_orthogonal`, `coe_iSup`
`map` 📖	CompOp	3 math math: `map_id`, `gc_map_comap`, `map_le_iff_le_comap`
`mapEquiv` 📖	CompOp	9 math math: `mapEquiv_sup_eq`, `mapEquiv_top_eq_top`, `mapEquiv_symm`, `mapEquiv_bot_eq_bot`, `closure_map_eq_mapEquiv_closure`, `mem_mapEquiv_iff'`, `mapEquiv_apply`, `mem_mapEquiv_iff`, `mapEquiv_inf_eq`
`toCloseds` 📖	CompOp	2 math math: `toCloseds_injective`, `coe_toCloseds`
`toSubmodule` 📖	CompOp	36 math math: `toSubmodule_orthogonal_eq`, `mem_iff`, `toSubmodule_sup`, `coe_sSup`, `Submodule.instHasOrthogonalProjectionOfCompleteSpace`, `mem_toSubmodule_iff`, `Submodule.closure_eq`, `toSubmodule_iSup`, `ext_iff`, `orthogonal_eq_inter`, `toSubmodule_iInf`, `Submodule.closure_le`, `mem_orthogonal_toSubmodule_iff`, `mem_sup`, `toSubmodule_injective`, `mem_iSup`, `mem_orthogonal_iff`, `toSubmodule_sSup`, `toSubmodule_comap`, `toSubmodule_le_toSubmodule`, `mem_sSup`, `mapEquiv_apply`, `orthogonal_toSubmodule_eq`, `instCanLiftSubmoduleToSubmoduleIsClosedCoe`, `toSubmodule_bot`, `toSubmodule_inf`, `coe_iSup`, `toSubmodule_top`, `orthogonal_closure`, `ProperCone.innerDual_toSubmodule`, `toSubmodule_sInf`, `coe_sup`, `carrier_eq_coe`, `coe_toSubmodule`, `closure_toSubmodule_eq`, `isClosed'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`carrier_eq_coe` 📖	mathematical	—	`AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.toAddSubsemigroup` `Submodule.toAddSubmonoid` `toSubmodule` `SetLike.coe` `ClosedSubmodule` `instSetLike`	—	—
`closure_map_eq_mapEquiv_closure` 📖	mathematical	—	`Submodule.closure` `Submodule.map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `ContinuousLinearEquiv.toLinearEquiv` `DFunLike.coe` `Equiv` `ClosedSubmodule` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv`	—	`RingHomInvPair.ids` `ext` `RingHomSurjective.ids` `Set.ext` `Set.image_congr` `ContinuousLinearEquiv.image_closure`
`closure_toSubmodule_eq` 📖	mathematical	—	`Submodule.closure` `toSubmodule`	—	`ext` `Set.ext` `Submodule.closure_eq`
`coe_bot` 📖	mathematical	—	`SetLike.coe` `ClosedSubmodule` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBot` `Set` `Set.instSingletonSet` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`coe_comap` 📖	mathematical	—	`SetLike.coe` `ClosedSubmodule` `instSetLike` `comap` `Set.preimage` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	—	—
`coe_iInf` 📖	mathematical	—	`SetLike.coe` `ClosedSubmodule` `instSetLike` `iInf` `instInfSet` `Set` `Set.instInfSet`	—	`toSubmodule_iInf` `Submodule.coe_iInf`
`coe_iSup` 📖	mathematical	—	`SetLike.coe` `ClosedSubmodule` `instSetLike` `iSup` `instSupSet` `closure` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.toAddSubsemigroup` `Submodule.toAddSubmonoid` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `toSubmodule`	—	`toSubmodule_iSup`
`coe_inf` 📖	mathematical	—	`SetLike.coe` `ClosedSubmodule` `instSetLike` `instInf` `Set` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra`	—	—
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `ClosedSubmodule` `instSetLike` `InfSet.sInf` `instInfSet` `iInf` `Set` `Set.instInfSet` `Set.instMembership`	—	`Submodule.coe_iInf` `iInf_congr_Prop`
`coe_sSup` 📖	mathematical	—	`SetLike.coe` `ClosedSubmodule` `instSetLike` `SupSet.sSup` `instSupSet` `closure` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.toAddSubsemigroup` `Submodule.toAddSubmonoid` `iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Set` `Set.instMembership` `toSubmodule`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `ClosedSubmodule` `instSetLike` `instMax` `closure` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.toAddSubsemigroup` `Submodule.toAddSubmonoid` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `toSubmodule`	—	—
`coe_toCloseds` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `TopologicalSpace.Closeds.instSetLike` `toCloseds` `ClosedSubmodule` `instSetLike`	—	—
`coe_toSubmodule` 📖	mathematical	—	`SetLike.coe` `Submodule` `Submodule.setLike` `toSubmodule` `ClosedSubmodule` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `ClosedSubmodule` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderTop` `Set.univ`	—	—
`comap_comap` 📖	mathematical	—	`comap` `ContinuousLinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	—
`comap_id` 📖	mathematical	—	`comap` `ContinuousLinearMap.id`	—	—
`ext` 📖	—	`AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.toAddSubsemigroup` `Submodule.toAddSubmonoid` `toSubmodule`	—	—	—
`ext_iff` 📖	mathematical	—	`AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.toAddSubsemigroup` `Submodule.toAddSubmonoid` `toSubmodule`	—	`ext`
`gc_map_comap` 📖	mathematical	—	`GaloisConnection` `ClosedSubmodule` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`map_le_iff_le_comap`
`instAddSubmonoidClass` 📖	mathematical	—	`AddSubmonoidClass` `ClosedSubmodule` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instSetLike`	—	`Submodule.add_mem` `Submodule.zero_mem`
`instCanLiftSubmoduleToSubmoduleIsClosedCoe` 📖	mathematical	—	`CanLift` `Submodule` `ClosedSubmodule` `toSubmodule` `IsClosed` `SetLike.coe` `Submodule.setLike`	—	—
`instSMulMemClass` 📖	mathematical	—	`SMulMemClass` `ClosedSubmodule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instSetLike`	—	`Submodule.smul_mem`
`isClosed` 📖	mathematical	—	`IsClosed` `SetLike.coe` `ClosedSubmodule` `instSetLike`	—	`isClosed'`
`isClosed'` 📖	mathematical	—	`IsClosed` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.toAddSubsemigroup` `Submodule.toAddSubmonoid` `toSubmodule`	—	—
`mapEquiv_apply` 📖	mathematical	—	`toSubmodule` `DFunLike.coe` `Equiv` `ClosedSubmodule` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv` `Submodule.map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `ContinuousLinearEquiv.toLinearEquiv`	—	`RingHomInvPair.ids`
`mapEquiv_bot_eq_bot` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ClosedSubmodule` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBot`	—	`RingHomInvPair.ids` `ext` `Set.ext` `Submodule.map_bot` `RingHomSurjective.ids`
`mapEquiv_inf_eq` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ClosedSubmodule` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv` `instInf`	—	`RingHomInvPair.ids` `ext` `Set.ext`
`mapEquiv_sup_eq` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ClosedSubmodule` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv` `instMax`	—	`RingHomInvPair.ids` `ext` `Set.ext` `RingHomSurjective.ids` `Set.image_congr` `LinearMap.ext` `Submodule.coe_closure` `Submodule.map_sup` `Submodule.map_coe`
`mapEquiv_symm` 📖	mathematical	—	`mapEquiv` `ContinuousLinearEquiv.symm` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Equiv.symm` `ClosedSubmodule`	—	`RingHomInvPair.ids`
`mapEquiv_top_eq_top` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ClosedSubmodule` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderTop`	—	`RingHomInvPair.ids` `ext` `Set.ext` `RingHomSurjective.ids` `Submodule.map_top` `LinearEquiv.range`
`map_id` 📖	mathematical	—	`map` `ContinuousLinearMap.id`	—	`SetLike.coe_injective` `RingHomSurjective.ids` `Submodule.closure.congr_simp` `Submodule.map_id` `Submodule.closure_eq`
`map_le_iff_le_comap` 📖	mathematical	—	`ClosedSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`RingHomSurjective.ids`
`mem_bot` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBot` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`mem_comap` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `comap` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	—	—
`mem_iInf` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet`	—	`coe_iInf`
`mem_iSup` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `iSup` `instSupSet` `Set` `Set.instMembership` `closure` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.toAddSubsemigroup` `Submodule.toAddSubmonoid` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `toSubmodule`	—	`coe_iSup`
`mem_inf` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `instInf`	—	—
`mem_mapEquiv_iff` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm`	—	`RingHomInvPair.ids` `Submodule.mem_map_equiv`
`mem_mapEquiv_iff'` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousLinearEquiv.equivLike`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.symm_apply_apply`
`mem_mk` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `Submodule` `Submodule.setLike`	—	—
`mem_sInf` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`coe_sInf`
`mem_sSup` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `SupSet.sSup` `instSupSet` `Set` `Set.instMembership` `closure` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.toAddSubsemigroup` `Submodule.toAddSubmonoid` `iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `toSubmodule`	—	—
`mem_sup` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `instMax` `Set` `Set.instMembership` `closure` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.toAddSubsemigroup` `Submodule.toAddSubmonoid` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `toSubmodule`	—	—
`mem_toSubmodule_iff` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `toSubmodule` `ClosedSubmodule` `instSetLike`	—	—
`mem_top` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderTop`	—	—
`toCloseds_injective` 📖	mathematical	—	`ClosedSubmodule` `TopologicalSpace.Closeds` `toCloseds`	—	`SetLike.coe_injective`
`toSubmodule_bot` 📖	mathematical	—	`toSubmodule` `Bot.bot` `ClosedSubmodule` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBot` `Submodule` `Submodule.instBot`	—	—
`toSubmodule_comap` 📖	mathematical	—	`toSubmodule` `comap` `Submodule.comap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.toLinearMap`	—	—
`toSubmodule_iInf` 📖	mathematical	—	`toSubmodule` `iInf` `ClosedSubmodule` `instInfSet` `Submodule` `Submodule.instInfSet`	—	`iInf.eq_1` `toSubmodule_sInf` `iInf_range`
`toSubmodule_iSup` 📖	mathematical	—	`toSubmodule` `iSup` `ClosedSubmodule` `instSupSet` `Submodule.closure` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`iSup.eq_1` `toSubmodule_sSup` `iSup_range`
`toSubmodule_inf` 📖	mathematical	—	`toSubmodule` `ClosedSubmodule` `instInf` `Submodule` `Submodule.instMin`	—	—
`toSubmodule_injective` 📖	mathematical	—	`ClosedSubmodule` `Submodule` `toSubmodule`	—	`isClosed'`
`toSubmodule_le_toSubmodule` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `toSubmodule` `ClosedSubmodule` `instPartialOrder`	—	—
`toSubmodule_sInf` 📖	mathematical	—	`toSubmodule` `InfSet.sInf` `ClosedSubmodule` `instInfSet` `iInf` `Submodule` `Submodule.instInfSet` `Set` `Set.instMembership`	—	—
`toSubmodule_sSup` 📖	mathematical	—	`toSubmodule` `SupSet.sSup` `ClosedSubmodule` `instSupSet` `Submodule.closure` `iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Set` `Set.instMembership`	—	—
`toSubmodule_sup` 📖	mathematical	—	`toSubmodule` `ClosedSubmodule` `instMax` `Submodule.closure` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	—
`toSubmodule_top` 📖	mathematical	—	`toSubmodule` `Top.top` `ClosedSubmodule` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderTop` `Submodule` `Submodule.instTop`	—	—

Submodule

Definitions

Name	Category	Theorems
`closure` 📖	CompOp	13 math math: `closure_eq'`, `ClosedSubmodule.toSubmodule_sup`, `ClosedSubmodule.orthogonal_closure''`, `closure_eq`, `ClosedSubmodule.closure_map_eq_mapEquiv_closure`, `ClosedSubmodule.toSubmodule_iSup`, `closure_le`, `ClosedSubmodule.toSubmodule_sSup`, `coe_closure`, `ClosedSubmodule.orthogonal_closure`, `ClosedSubmodule.orthogonal_closure'`, `ClosedSubmodule.closure_toSubmodule_eq`, `mem_closure_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq` 📖	mathematical	—	`closure` `ClosedSubmodule.toSubmodule`	—	`ClosedSubmodule.ext` `Set.ext` `closure_eq_iff_isClosed` `ClosedSubmodule.isClosed'`
`closure_eq'` 📖	mathematical	—	`closure`	—	`ClosedSubmodule.ext` `Set.ext` `IsClosed.closure_eq`
`closure_le` 📖	mathematical	—	`ClosedSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `ClosedSubmodule.instPartialOrder` `closure` `Submodule` `instPartialOrder` `ClosedSubmodule.toSubmodule`	—	`IsClosed.closure_subset_iff` `ClosedSubmodule.isClosed`
`coe_closure` 📖	mathematical	—	`SetLike.coe` `ClosedSubmodule` `ClosedSubmodule.instSetLike` `closure` `closure` `Submodule` `setLike`	—	—
`mem_closure_iff` 📖	mathematical	—	`ClosedSubmodule` `SetLike.instMembership` `ClosedSubmodule.instSetLike` `closure` `Submodule` `setLike` `topologicalClosure`	—	—

(root)

Definitions

Name	Category	Theorems
`ClosedSubmodule` 📖	CompData	93 math math: `ClosedSubmodule.mapEquiv_sup_eq`, `ClosedSubmodule.mapEquiv_top_eq_top`, `StandardSubspace.toClosedSubmodule_injective`, `ClosedSubmodule.sub_mem_orthogonal_of_inner_right`, `ClosedSubmodule.mem_iff`, `ClosedSubmodule.toCloseds_injective`, `ClosedSubmodule.mem_comap`, `ProperCone.innerDual_univ`, `ClosedSubmodule.orthogonal_gc`, `ClosedSubmodule.toSubmodule_sup`, `ProperCone.coe_positive`, `ClosedSubmodule.mem_orthogonal'`, `ClosedSubmodule.coe_sSup`, `ClosedSubmodule.inf_orthogonal`, `ClosedSubmodule.mem_iInf`, `ClosedSubmodule.instSMulMemClass`, `ClosedSubmodule.orthogonal_injective`, `ProperCone.coe_bot`, `ClosedSubmodule.mem_bot`, `ClosedSubmodule.mapEquiv_symm`, `ClosedSubmodule.mem_toSubmodule_iff`, `ClosedSubmodule.mapEquiv_bot_eq_bot`, `ProperCone.innerDual_zero`, `ClosedSubmodule.orthogonal_le`, `ClosedSubmodule.mulI_sup`, `ClosedSubmodule.coe_sInf`, `ClosedSubmodule.bot_orthogonal_eq_top`, `StandardSubspace.IsSeparating`, `ClosedSubmodule.closure_map_eq_mapEquiv_closure`, `ClosedSubmodule.top_orthogonal_eq_bot`, `ClosedSubmodule.toSubmodule_iSup`, `ClosedSubmodule.mem_mapEquiv_iff'`, `ProperCone.dual_univ`, `ClosedSubmodule.orthogonal_eq_inter`, `StandardSubspace.IsCyclic`, `ClosedSubmodule.coe_bot`, `ClosedSubmodule.orthogonal_orthogonal_monotone`, `ClosedSubmodule.mem_inf`, `ClosedSubmodule.mem_symplComp_iff`, `ClosedSubmodule.toSubmodule_iInf`, `ClosedSubmodule.iInf_orthogonal`, `ClosedSubmodule.coe_toCloseds`, `ClosedSubmodule.sup_orthogonal`, `ClosedSubmodule.sub_mem_orthogonal_of_inner_left`, `Submodule.closure_le`, `ProperCone.dual_zero`, `ClosedSubmodule.mem_orthogonal`, `ClosedSubmodule.mulI_inf`, `ClosedSubmodule.mem_orthogonal_toSubmodule_iff`, `ClosedSubmodule.mem_sup`, `ClosedSubmodule.toSubmodule_injective`, `ClosedSubmodule.mem_iSup`, `ClosedSubmodule.gc_map_comap`, `ClosedSubmodule.orthogonal_eq_top_iff`, `ClosedSubmodule.mem_orthogonal_iff`, `ClosedSubmodule.coe_inf`, `ClosedSubmodule.toSubmodule_sSup`, `ClosedSubmodule.toSubmodule_le_toSubmodule`, `ProperCone.toPointedCone_bot`, `ClosedSubmodule.coe_iInf`, `ClosedSubmodule.isClosed`, `ClosedSubmodule.inf_orthogonal_eq_bot`, `ClosedSubmodule.mem_sSup`, `ClosedSubmodule.mem_sInf`, `ProperCone.innerDual_empty`, `ClosedSubmodule.mem_mk`, `ClosedSubmodule.sInf_orthogonal`, `ClosedSubmodule.map_le_iff_le_comap`, `ClosedSubmodule.mapEquiv_apply`, `ClosedSubmodule.instCanLiftSubmoduleToSubmoduleIsClosedCoe`, `ClosedSubmodule.mem_top`, `Submodule.coe_closure`, `ProperCone.mem_bot`, `ClosedSubmodule.toSubmodule_bot`, `ProperCone.dual_empty`, `ClosedSubmodule.mem_mapEquiv_iff`, `ClosedSubmodule.toSubmodule_inf`, `ClosedSubmodule.coe_top`, `ClosedSubmodule.orthogonal_disjoint`, `ClosedSubmodule.coe_iSup`, `ClosedSubmodule.toSubmodule_top`, `ClosedSubmodule.symplComp_sup`, `ClosedSubmodule.toSubmodule_sInf`, `ClosedSubmodule.coe_sup`, `instCompleteSpaceSubtypeMemClosedSubmodule`, `ClosedSubmodule.coe_comap`, `ClosedSubmodule.involutive_mulI`, `ClosedSubmodule.symplComp_inf`, `ClosedSubmodule.carrier_eq_coe`, `ClosedSubmodule.mapEquiv_inf_eq`, `ClosedSubmodule.coe_toSubmodule`, `ClosedSubmodule.instAddSubmonoidClass`, `Submodule.mem_closure_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompleteSpaceSubtypeMemClosedSubmodule` 📖	mathematical	—	`CompleteSpace` `ClosedSubmodule` `UniformSpace.toTopologicalSpace` `SetLike.instMembership` `ClosedSubmodule.instSetLike` `instUniformSpaceSubtype`	—	`IsComplete.completeSpace_coe` `ClosedSubmodule.carrier_eq_coe` `IsClosed.isComplete` `ClosedSubmodule.isClosed'`

---

← Back to Index