Auxiliary theorems about ContinuousLinearMap

Mostly about ContinuousLinearMap.IsInvertible and ContinuousLinearMap.inverse.

@[simp]

theorem ContinuousLinearMap.IsInvertible.self_comp_inverse {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] {f : E →L[R] F} (hf : f.IsInvertible) : f.comp f.inverse = ContinuousLinearMap.id R F

@[simp]

theorem ContinuousLinearMap.IsInvertible.inverse_comp_self {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] {f : E →L[R] F} (hf : f.IsInvertible) : f.inverse.comp f = ContinuousLinearMap.id R E

theorem ContinuousLinearMap.IsInvertible.bijective {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] {f : E →L[R] F} (hf : f.IsInvertible) : Function.Bijective ⇑f

theorem ContinuousLinearMap.IsInvertible.injective {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] {f : E →L[R] F} (hf : f.IsInvertible) : Function.Injective ⇑f

theorem ContinuousLinearMap.IsInvertible.surjective {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] {f : E →L[R] F} (hf : f.IsInvertible) : Function.Surjective ⇑f

theorem ContinuousLinearMap.IsInvertible.inverse {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] {f : E →L[R] F} (hf : f.IsInvertible) : f.inverse.IsInvertible

theorem ContinuousLinearMap.IsInvertible.of_isInvertible_inverse {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] {f : E →L[R] F} (hf : f.inverse.IsInvertible) : f.IsInvertible

@[simp]

theorem ContinuousLinearMap.isInvertible_inverse_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] [TopologicalSpace E] [TopologicalSpace F] {f : E →L[R] F} : f.inverse.IsInvertible ↔ f.IsInvertible