Theorems · Theorem · functional analysis

LinearMap.IsWeak.congr

∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {E' : Type u_5} {F' : Type u_6} [inst : CommSemiring 𝕜]
  [inst_1 : TopologicalSpace 𝕜] [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F]
  [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace E] [inst_7 : AddCommMonoid E'] [inst_8 : Module 𝕜 E']
  [inst_9 : AddCommMonoid F'] [inst_10 : Module 𝕜 F'] [inst_11 : TopologicalSpace E'] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
  (B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜) (e : E ≃L[𝕜] E') (f : F ≃ₗ[𝕜] F'),
  ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B' → ∀ [hB : B.IsWeak], B'.IsWeak

Suppose B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜 and B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜 are bilinear maps such that E ≃L[𝕜] E' and F ≃ₗ[𝕜] F'. If B.IsWeak, then so also B'.IsWeak.

Defined in

Mathlib.Topology.Algebra.Module.IsWeak

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringTopologicalSpaceAddCommMonoidModuleAddCommMonoidModuleTopologicalSpaceAddCommMonoidModuleAddCommMonoidModuleTopologicalSpaceLinearMap.IsWeak