Theorems · Theorem · functional analysis

LinearPMap.closure_inverse_graph

∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  {f : E →ₗ.[R] F} [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R]
  [inst_10 : ContinuousSMul R E] [inst_11 : ContinuousSMul R F],
  f.toFun.ker = ⊥ →
    f.IsClosable → f.closure.toFun.ker = ⊥ → f.closure.inverse.graph = f.inverse.graph.topologicalClosure

If f is invertible and closable as well as its closure being invertible, then the graph of the inverse of the closure is given by the closure of the graph of the inverse.

Defined in

Mathlib.Topology.Algebra.Module.LinearPMap

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupModuleModuleTopologicalSpaceTopologicalSpaceContinuousAddContinuousAddTopologicalSpaceContinuousSMulContinuousSMul