Theorems · Theorem · functional analysis

ClosedSubmodule.closure_map_eq_mapEquiv_closure

∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] (f : M ≃L[R] N) [inst_7 : ContinuousAdd N] [inst_8 : ContinuousConstSMul R N]
  [inst_9 : ContinuousAdd M] [inst_10 : ContinuousConstSMul R M] (s : Submodule R M),
  (Submodule.map (↑↑f) s).closure = (ClosedSubmodule.mapEquiv f) s.closure

Defined in

Mathlib.Topology.Algebra.Module.ClosedSubmodule

Cited by

0 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidTopologicalSpaceModuleAddCommMonoidTopologicalSpaceModuleContinuousAddContinuousConstSMulContinuousAddContinuousConstSMul