LinearMap.polar_gc
theorem 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)
This theorem states that for a given linear map `B` from type `E` to type `F` over a normed commutative ring `π`, there exists a Galois connection between the polar of `B` and the polar of the flipped version of `B`. This connection is formed by applying the `toDual` function of the `OrderDual` (a structure that reverses the order of a given ordered set) to the polar of `B` and the `ofDual` function of the `OrderDual` to the polar of the flipped version of `B`. This expresses that the `polar` function is order-reversing, meaning that an increase in the original set implies a decrease in the polar set, and vice versa.
More concisely: For a linear map B from type E to type F over a normed commutative ring, there exists a Galois connection between the polar of B and the polar of the flipped version of B, given by applying the OrderDual.toDual to the polar of B and OrderDual.ofDual to the polar of the flipped version of B.
|
LinearMap.polar_weak_closed
theorem LinearMap.polar_weak_closed :
β {π : 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 ββ[π] π) (s : Set E),
IsClosed (B.polar s)
The theorem `LinearMap.polar_weak_closed` asserts that for any normed commutative ring `π`, additive commutative monoids `E` and `F`, and modules `E` and `F` over `π`, along with a bilinear map `B` from `E` to `F` and a set of elements from `E` (denoted as `s`), the polar set of `s` with respect to `B` is a closed set in the weak topology induced by the flipped version of the bilinear map `B`.
More concisely: The polar set of a set with respect to a bilinear form is weakly closed in the corresponding normed spaces.
|