Theorems · Theorem · functional analysis

LinearMap.polar_gc

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜),
  GaloisConnection (⇑OrderDual.toDual ∘ B.polar) (B.flip.polar ∘ ⇑OrderDual.ofDual)

The map B.polar : Set E → Set F forms an order-reversing Galois connection with B.flip.polar : Set F → Set E. We use OrderDual.toDual and OrderDual.ofDual to express that polar is order-reversing.

Defined in

Mathlib.Analysis.LocallyConvex.Polar

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedCommRingAddCommMonoidAddCommMonoidModuleModule