LeanPool.Monlib4.LinearAlgebra.OfNorm

Imported Lean Pool material for LeanPool.Monlib4.LinearAlgebra.OfNorm.

theorem cs_aux {𝕜 : Type u_2} {E : Type u_1} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} (hy : y ≠ 0) : ‖x - (inner 𝕜 y x * ↑(‖y‖ ^ 2)⁻¹) • y‖ ^ 2 = ‖x‖ ^ 2 - ‖inner 𝕜 x y‖ ^ 2 * (‖y‖ ^ 2)⁻¹

noncomputable def OfNorm.innerDef {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (x y : X) : 𝕜

Polarization expression used to recover an inner product from a norm.

Equations

• OfNorm.innerDef x y = 4⁻¹ * (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + RCLike.I * ↑‖RCLike.I • x + y‖ ^ 2 - RCLike.I * ↑‖RCLike.I • x - y‖ ^ 2)

theorem OfNorm.re_innerDef {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (x y : X) : RCLike.re (innerDef x y) = 4⁻¹ * (‖x + y‖ ^ 2 - ‖x - y‖ ^ 2)

theorem OfNorm.im_eq_re_neg_i {𝕜 : Type u_1} [RCLike 𝕜] (x : 𝕜) : RCLike.im x = RCLike.re (-RCLike.I * x)

theorem OfNorm.innerDef_zero_left {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (x : X) : innerDef 0 x = 0

theorem OfNorm.innerDef_i_smul_left {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (x y : X) : innerDef (RCLike.I • x) y = -RCLike.I * innerDef x y

theorem OfNorm.im_innerDef_aux {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (x y : X) : RCLike.im (innerDef x y) = RCLike.re (innerDef (RCLike.I • x) y)

theorem OfNorm.re_innerDef_symm {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (x y : X) : RCLike.re (innerDef x y) = RCLike.re (innerDef y x)

theorem OfNorm.im_innerDef_symm {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (x y : X) : RCLike.im (innerDef x y) = -RCLike.im (innerDef y x)

theorem OfNorm.innerDef_conj {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (x y : X) : (starRingEnd 𝕜) (innerDef x y) = innerDef y x

def IsContinuousLinearMap (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) : Prop

An unbundled continuous linear map predicate.

Equations

• IsContinuousLinearMap 𝕜 f = (IsLinearMap 𝕜 f ∧ Continuous f)

def IsContinuousLinearMap.mk' {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (h : IsContinuousLinearMap 𝕜 f) : E →L[𝕜] F

Bundle an unbundled continuous linear map as a continuous linear map.

Equations

• h.mk' = { toLinearMap := IsLinearMap.mk' f ⋯, cont := ⋯ }

theorem IsContinuousLinearMap.coe_mk' {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (h : IsContinuousLinearMap 𝕜 f) : f = ⇑h.mk'

theorem isBoundedLinearMap_iff_isContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) : IsBoundedLinearMap 𝕜 f ↔ IsContinuousLinearMap 𝕜 f

def WithBound {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] (f : E → F) : Prop

A function has a linear norm bound.

Equations

• WithBound f = ∃ (M : ℝ), 0 < M ∧ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖

theorem IsBoundedLinearMap.def {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} : IsBoundedLinearMap 𝕜 f ↔ IsLinearMap 𝕜 f ∧ WithBound f

theorem LinearMap.withBound_iff_is_continuous {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E →ₗ[𝕜] F} : WithBound ⇑f ↔ Continuous ⇑f

theorem LinearMap.ker_coe_def {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] {f : E →ₗ[R] F} : ↑f.ker = {x : E | f x = 0}

theorem exists_dual_vector_of_ne {𝕜 : Type u_2} [RCLike 𝕜] {X : Type u_1} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {x y : X} (h : x ≠ y) : ∃ (f : StrongDual 𝕜 X), f x ≠ f y

theorem isLinearMap_zero (R : Type u_1) {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] : IsLinearMap R 0

theorem isContinuousLinearMapZero {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] : IsContinuousLinearMap 𝕜 0

theorem IsContinuousLinearMap.ofInnerSymmetricFun {𝕜 : Type u_2} [RCLike 𝕜] {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace 𝕜 X] [CompleteSpace X] {f : X → X} (h : ∀ (a b : X), inner 𝕜 (f a) b = inner 𝕜 a (f b)) : IsContinuousLinearMap 𝕜 f

structure IsBilinearMapProd (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E × F → G) : Prop

Bilinearity for maps whose domain is a product type.

• add_left (x₁ x₂ : E) (y : F) : f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y)
• smul_left (c : 𝕜) (x : E) (y : F) : f (c • x, y) = c • f (x, y)
• add_right (x : E) (y₁ y₂ : F) : f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂)
• smul_right (c : 𝕜) (x : E) (y : F) : f (x, c • y) = c • f (x, y)

def IsLeftLinearMap (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E × F → G) : Prop

Linearity of a product map in its left argument.

Equations

• IsLeftLinearMap 𝕜 f = ∀ (b : F), IsLinearMap 𝕜 fun (a : E) => f (a, b)

theorem isLeftLinearMap_iff {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} : IsLeftLinearMap 𝕜 f ↔ ∀ (b : F), IsLinearMap 𝕜 fun (a : E) => f (a, b)

def IsRightLinearMap (𝕜 : Type u_1) [NormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : E × F → G) : Prop

Linearity of a product map in its right argument.

Equations

• IsRightLinearMap 𝕜 f = ∀ (a : E), IsLinearMap 𝕜 fun (b : F) => f (a, b)

theorem isRightLinearMap_iff {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} : IsRightLinearMap 𝕜 f ↔ ∀ (a : E), IsLinearMap 𝕜 fun (b : F) => f (a, b)

theorem isBilinearMap_iff_is_linear_map_left_right {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} : IsBilinearMapProd 𝕜 f ↔ IsLeftLinearMap 𝕜 f ∧ IsRightLinearMap 𝕜 f

def IsBilinearMapProd.toLmLm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} (hf : IsBilinearMapProd 𝕜 f) : E →ₗ[𝕜] F →ₗ[𝕜] G

Bundle a product bilinear map as a linear map into linear maps.

Equations

• hf.toLmLm = { toFun := fun (x : E) => { toFun := fun (y : F) => f (x, y), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

def IsLmLeftIsClmRight.toLmClm {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} (hf₁ : ∀ (y : F), IsLinearMap 𝕜 fun (a : E) => f (a, y)) (hf₂ : ∀ (x : E), IsContinuousLinearMap 𝕜 fun (a : F) => f (x, a)) : E →ₗ[𝕜] F →L[𝕜] G

Bundle a product map that is left-linear and right-continuous-linear.

Equations

• IsLmLeftIsClmRight.toLmClm hf₁ hf₂ = { toFun := fun (x : E) => ⋯.mk', map_add' := ⋯, map_smul' := ⋯ }

theorem IsBilinearMapProd.zero_left {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} (h : IsBilinearMapProd 𝕜 f) (y : F) : f (0, y) = 0

theorem IsBilinearMapProd.zero_right {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} (h : IsBilinearMapProd 𝕜 f) (x : E) : f (x, 0) = 0

theorem IsBilinearMapProd.eq_zero_add_self {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} (h : IsBilinearMapProd 𝕜 f) (xy : E × F) : f xy = f (xy.1, 0) + f xy

def IsBilinearMap.toLmLm {𝕜 : Type u_1} [CommSemiring 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] {F : Type u_3} [AddCommMonoid F] [Module 𝕜 F] {G : Type u_4} [AddCommMonoid G] [Module 𝕜 G] {f : E → F → G} (hf : IsBilinearMap 𝕜 f) : E →ₗ[𝕜] F →ₗ[𝕜] G

Compatibility alias for the curried linear map associated to a bilinear map.

Equations

• hf.toLmLm = hf.toLinearMap

theorem IsBilinearMap.zero_left {𝕜 : Type u_1} [CommSemiring 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] {F : Type u_3} [AddCommMonoid F] [Module 𝕜 F] {G : Type u_4} [AddCommMonoid G] [Module 𝕜 G] {f : E → F → G} (h : IsBilinearMap 𝕜 f) (y : F) : f 0 y = 0

theorem IsBilinearMap.zero_right {𝕜 : Type u_1} [CommSemiring 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] {F : Type u_3} [AddCommMonoid F] [Module 𝕜 F] {G : Type u_4} [AddCommMonoid G] [Module 𝕜 G] {f : E → F → G} (h : IsBilinearMap 𝕜 f) (x : E) : f x 0 = 0

theorem IsBilinearMap.eq_zero_add_self {𝕜 : Type u_1} [CommSemiring 𝕜] {E : Type u_2} [AddCommMonoid E] [Module 𝕜 E] {F : Type u_3} [AddCommMonoid F] [Module 𝕜 F] {G : Type u_4} [AddCommMonoid G] [Module 𝕜 G] {f : E → F → G} (h : IsBilinearMap 𝕜 f) (x : E) (y : F) : f x y = f x 0 + f x y

theorem IsContinuousLinearMap.to_is_lm {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} [NormedField 𝕜] [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace 𝕜 X] [NormedSpace 𝕜 Y] {β : X → Y} (hf : IsContinuousLinearMap 𝕜 β) : IsLinearMap 𝕜 β

theorem Set.mem_extremePoints_iff' {𝕜 : Type u_2} [RCLike 𝕜] {H : Type u_1} [AddCommMonoid H] [SMul 𝕜 H] (x : H) (y : Set H) : x ∈ extremePoints 𝕜 y ↔ x ∈ y ∧ ∀ x₁ ∈ y, ∀ x₂ ∈ y, (∃ (a : 𝕜), 0 < a ∧ a < 1 ∧ a • x₁ + (1 - a) • x₂ = x) → x₁ = x ∧ x₂ = x

theorem Metric.mem_extremePoints_of_closed_unitBall_iff {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] (x : H) : x ∈ Set.extremePoints 𝕜 (closedBall 0 1) ↔ ‖x‖ ≤ 1 ∧ ∀ (x₁ : H), ‖x₁‖ ≤ 1 → ∀ (x₂ : H), ‖x₂‖ ≤ 1 → (∃ (a : 𝕜), 0 < a ∧ a < 1 ∧ a • x₁ + (1 - a) • x₂ = x) → x₁ = x ∧ x₂ = x

theorem Metric.mem_extremePoints_of_unitBall_iff {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] (x : H) : x ∈ Set.extremePoints 𝕜 (ball 0 1) ↔ ‖x‖ < 1 ∧ ∀ (x₁ : H), ‖x₁‖ < 1 → ∀ (x₂ : H), ‖x₂‖ < 1 → (∃ (a : 𝕜), 0 < a ∧ a < 1 ∧ a • x₁ + (1 - a) • x₂ = x) → x₁ = x ∧ x₂ = x

theorem Metric.exists_mem_closed_unitBall_of_norm_one (𝕜 : Type u_1) (H : Type u_2) [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] [Nontrivial H] : ∃ (x : H), ‖x‖ = 1 ∧ x ∈ closedBall 0 1

theorem Metric.exists_mem_unitBall_of_norm_one (𝕜 : Type u_1) (H : Type u_2) [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] [Nontrivial H] : ∃ (x : H) (ε : ℝ), ‖x‖ = ε ∧ 0 < ε ∧ ε < 1 ∧ x ∈ ball 0 1

theorem inner_lt_one_iff_of_norm_one {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {x y : H} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : inner 𝕜 x y < 1 ↔ x ≠ y ∧ ↑(RCLike.re (inner 𝕜 x y)) = inner 𝕜 x y

theorem re_inner_lt_one_iff_of_norm_one {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {x y : H} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : RCLike.re (inner 𝕜 x y) < 1 ↔ x ≠ y

theorem ne_zero_iff_nontrivial_of_mem_extremePoints_closed_unitBall {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {x : H} (hx : x ∈ Set.extremePoints 𝕜 (Metric.closedBall 0 1)) : x ≠ 0 ↔ Nontrivial H

theorem norm_one_of_mem_extremePoints_of_closed_unitBall {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [NormedSpace 𝕜 H] [Nontrivial H] {x : H} (hx : x ∈ Set.extremePoints 𝕜 (Metric.closedBall 0 1)) : ‖x‖ = 1

theorem mem_extremePoints_of_closedBall_iff_norm_eq_one {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Nontrivial H] (x : H) : x ∈ Set.extremePoints 𝕜 (Metric.closedBall 0 1) ↔ ‖x‖ = 1

theorem LinearIsometry.norm_comp_toContinuousLinearMap_le {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RCLike 𝕜] [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 X] [NormedSpace 𝕜 Y] [NormedSpace 𝕜 Z] (f : X →ₗᵢ[𝕜] Y) (h : Y →L[𝕜] Z) : ‖h ∘SL f.toContinuousLinearMap‖ ≤ ‖h‖

def NormedSpace.Dual.transpose {E : Type u_1} {F : Type u_2} (𝕜 : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) : StrongDual 𝕜 F →ₗ[𝕜] StrongDual 𝕜 E

Pull back continuous linear functionals along a continuous linear map.

Equations

• NormedSpace.Dual.transpose 𝕜 f = { toFun := fun (x : StrongDual 𝕜 F) => x ∘SL f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem NormedSpace.Dual.transpose_apply {E : Type u_1} {F : Type u_2} (𝕜 : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : StrongDual 𝕜 F) : (transpose 𝕜 f) x = x ∘SL f

theorem NormedSpace.Dual.transpose_isometry {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} [RCLike 𝕜] [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedSpace 𝕜 X] [NormedSpace 𝕜 Y] {f : X ≃ₗᵢ[𝕜] Y} : Isometry ⇑(transpose 𝕜 f.toLinearIsometry.toContinuousLinearMap)

noncomputable def LinearEquiv.transpose {E : Type u_1} {F : Type u_2} (𝕜 : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) : StrongDual 𝕜 F ≃ₗᵢ[𝕜] StrongDual 𝕜 E

Pull back continuous linear functionals along a linear isometry equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.transpose_symm_apply {E : Type u_1} {F : Type u_2} (𝕜 : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) (a : StrongDual 𝕜 E) : (transpose 𝕜 f).symm a = (NormedSpace.Dual.transpose 𝕜 f.symm.toLinearIsometry.toContinuousLinearMap) a

@[simp]

theorem LinearEquiv.transpose_apply {E : Type u_1} {F : Type u_2} (𝕜 : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) (a : StrongDual 𝕜 F) : (transpose 𝕜 f) a = (NormedSpace.Dual.transpose 𝕜 f.toLinearIsometry.toContinuousLinearMap) a

theorem Set.subset_diff_inj {α : Type u_1} (s : Set α) {t u : Set α} (h : u ⊆ t) : s ⊆ t ↔ s \ u ⊆ t \ u

theorem example_pos_commute_iff_pos_mul_of {𝕜 : Type u_1} {R : Type u_2} [RCLike 𝕜] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [Algebra 𝕜 R] (h₁ : ∀ (x : R), 0 ≤ x ↔ ∃ (r : R), x = star r * r) (h₂ : ∀ (x : R), 0 ≤ x ↔ IsSelfAdjoint x ∧ spectrum 𝕜 x ⊆ {a : 𝕜 | 0 ≤ a}) {x y : R} (hx : 0 ≤ x) (hy : 0 ≤ y) : Commute x y ↔ 0 ≤ x * y