Submodule.orthogonal_disjoint
theorem Submodule.orthogonal_disjoint :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(K : Submodule 𝕜 E), Disjoint K K.orthogonal
The theorem states that for any field `𝕜`, and any inner product space `E` over `𝕜`, the intersection of any submodule `K` of `E` and its orthogonal complement `Kᗮ` is trivial. The term "trivial" in this context refers to the situation where the greatest element that belongs to both `K` and `Kᗮ` is the bottom element of the lattice, as defined in the `Disjoint` function. This is analogous to the idea of disjoint sets in set theory, where the intersection of disjoint sets is the empty set.
More concisely: For any field `𝕜` and inner product space `E` over `𝕜`, the intersection of a submodule `K` of `E` and its orthogonal complement `Kᗮ` is the zero submodule.
|
Submodule.mem_orthogonal
theorem Submodule.mem_orthogonal :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(K : Submodule 𝕜 E) (v : E), v ∈ K.orthogonal ↔ ∀ u ∈ K, ⟪u, v⟫_𝕜 = 0
This theorem states that for any type 𝕜, any normed additive commutative group E, and any inner product space with the scalar field 𝕜 and vector space E, a vector v is in the orthogonal complement of a submodule K of E (denoted as K.orthogonal) if and only if the inner product of v and any vector u in K is zero. In other words, v is orthogonal to every vector in K.
More concisely: A vector v is in the orthogonal complement of a submodule K of a normed additive commutative group and inner product space E over the same field, if and only if the inner product of v and any vector u in K equals zero.
|
Submodule.iInf_orthogonal
theorem Submodule.iInf_orthogonal :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{ι : Type u_4} (K : ι → Submodule 𝕜 E), ⨅ i, (K i).orthogonal = (iSup K).orthogonal
This theorem states that for any indexed family of orthogonal subspaces `K` of a normed add-commutative group `E` over a field `𝕜`, the infimum (greatest lower bound) of the orthogonals of each of these subspaces is equal to the orthogonal of the supremum (least upper bound) of the family `K`. This is in the context of inner product spaces, which are vector spaces with an additional structure that allows calculating angles and lengths.
More concisely: In an inner product space, the orthogonal complement of the supremum of an indexed family of orthogonal subspaces is equal to the infimum of the orthogonal complements of each subspace.
|
Submodule.IsOrtho.disjoint
theorem Submodule.IsOrtho.disjoint :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{U V : Submodule 𝕜 E}, U.IsOrtho V → Disjoint U V
The theorem "Submodule.IsOrtho.disjoint" states that for any types `𝕜` and `E`, where `𝕜` has a ring-like structure (`RCLike 𝕜`) and `E` is a normed additive commutative group (`NormedAddCommGroup E`) with an associated inner product space (`InnerProductSpace 𝕜 E`), if you have two submodules `U` and `V` of the vector space `E` over the field `𝕜`, then if `U` is orthogonal to `V` (`U.IsOrtho V`), `U` and `V` are disjoint. In other words, if two submodules are orthogonal, their greatest lower bound or infimum is the bottom element of the lattice structure.
More concisely: If `U` and `V` are orthogonal submodules of a normed additive commutative group `E` over a ring-like structure `𝕜`, then their intersection is the zero submodule `{0}`.
|
Submodule.top_orthogonal_eq_bot
theorem Submodule.top_orthogonal_eq_bot :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
⊤.orthogonal = ⊥
This theorem states that for any type `𝕜` (representing a scalar) and any type `E` (representing a vector space), given that `𝕜` forms a commutative ring (denoted by `RCLike 𝕜`), `E` forms a normed add commutative group, and `E` forms an inner product space over `𝕜`, the orthogonal complement of the entire space (`⊤ᗮ`) is the zero subspace (`⊥`). In the language of linear algebra, this means that the space orthogonal to the entire vector space is just the zero vector.
More concisely: If `𝕜` is a commutative ring, `E` a normed add commutative group and an inner product space over `𝕜`, then the orthogonal complement of `E` is the zero subspace.
|
Submodule.IsOrtho.mono_left
theorem Submodule.IsOrtho.mono_left :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{U₁ U₂ V : Submodule 𝕜 E}, U₂ ≤ U₁ → U₁.IsOrtho V → U₂.IsOrtho V
This theorem, `Submodule.IsOrtho.mono_left`, states that for any types 𝕜 and E, given 𝕜 is a ring-like structure, E is a normed additive commutative group, and E has an inner product structure over 𝕜, if we have two submodules U₁ and U₂ of E over 𝕜, and another submodule V of E over 𝕜, then if U₂ is a subset of U₁ and U₁ is orthogonal to V, it can be deduced that U₂ is also orthogonal to V. In mathematical terms, this states that orthogonality is preserved under taking subsets.
More concisely: If submodule U₂ is a subset of orthogonal submodule U₁ in a normed additive commutative group E over a ring-like structure 𝕜 with an inner product structure, then U₂ is orthogonal to V if U₁ is.
|
Submodule.inf_orthogonal
theorem Submodule.inf_orthogonal :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(K₁ K₂ : Submodule 𝕜 E), K₁.orthogonal ⊓ K₂.orthogonal = (K₁ ⊔ K₂).orthogonal
This theorem states that for any two subspaces `K₁` and `K₂` of an inner product space `E` over a base field `𝕜`, the intersection of the orthogonal complements of these subspaces (`K₁.orthogonal` and `K₂.orthogonal`) is equal to the orthogonal complement of the sum of the two subspaces (`(K₁ ⊔ K₂).orthogonal`). In simpler terms, the set of vectors that are orthogonal to both `K₁` and `K₂` is the same as the set of vectors that are orthogonal to the subspace formed by combining `K₁` and `K₂`.
More concisely: The orthogonal complements of subspaces K₁ and K₂ of an inner product space E over a base field ℝ have the same set of elements, i.e., K₁.orthogonal = K₂.orthogonal if and only if (K₁ ⊔ K₂).orthogonal.
|
Submodule.le_orthogonal_orthogonal
theorem Submodule.le_orthogonal_orthogonal :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(K : Submodule 𝕜 E), K ≤ K.orthogonal.orthogonal
This theorem states that for any type 𝕜 and E, where 𝕜 is RCLike and E is a NormedAddCommGroup and an InnerProductSpace over 𝕜, any submodule K of E is always contained within the double orthogonal complement of K, denoted as Kᗮᗮ. In other words, for any vector space E and its submodule K, the set of all vectors orthogonal to the orthogonal of K includes K itself.
More concisely: For any RCLike type 𝕜 and NormedAddCommGroup/InnerProductSpace 𝕎 over 𝕜, any submodule K of 𝕎 is contained in its double orthogonal complement Kᗮᗮ.
|
Submodule.orthogonal_eq_inter
theorem Submodule.orthogonal_eq_inter :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(K : Submodule 𝕜 E), K.orthogonal = ⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v)
The theorem `Submodule.orthogonal_eq_inter` states that for any field `𝕜` (which is equipped with a certain type of ordered field structure) and any normed add commutative group `E` (which is an inner product space over `𝕜`), the orthogonal of a submodule `K` of `E` can be characterized as the intersection of the kernels of the operations of inner product with each of the elements of `K`. In other words, each element of `K.orthogonal` is orthogonal to every element of `K` if and only if it gets mapped to zero by the linear map that takes an element of `E` and maps it to the result of the inner product with each element of `K`.
More concisely: The orthogonal complement of a submodule of a normed add commutative group equipped with an inner product over a field is the intersection of the kernels of the inner product with each element of the submodule.
|
Submodule.mem_orthogonal_singleton_iff_inner_right
theorem Submodule.mem_orthogonal_singleton_iff_inner_right :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{u v : E}, v ∈ (Submodule.span 𝕜 {u}).orthogonal ↔ ⟪u, v⟫_𝕜 = 0
This theorem states that for any vectors `u` and `v` in an inner product space `E` over a field `𝕜` (where `𝕜` satisfies the properties of RCLike), `v` is in the orthogonal complement of the subspace spanned by `u` if and only if the inner product of `u` and `v` is zero. In other words, a vector is in the orthogonal complement of the span of another vector if and only if it is orthogonal to that vector.
More concisely: For any inner product space E over field 𝕜, vector u orthogonal to vector v if and only if v lies in the orthogonal complement of the subspace spanned by u, that is, u ⊥ v if and only if v ∈ u⁊.
|
OrthogonalFamily.pairwise
theorem OrthogonalFamily.pairwise :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{ι : Type u_4} {V : ι → Submodule 𝕜 E},
(OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → Pairwise ((fun x x_1 => x.IsOrtho x_1) on V)
The theorem `OrthogonalFamily.pairwise` states that for any types `𝕜` and `E`, where `𝕜` behaves like a ring and `E` is a normed add commutative group over which we have an inner product space, and for any type `ι` and a function `V` mapping `ι` to a `Submodule` of `𝕜` and `E`, if the family of subspaces `V i` forms an `OrthogonalFamily`, then the relationship `x.IsOrtho x_1` holds pairwise over the subspaces `V`. In simpler terms, if we have a family of subspaces that are orthogonal to each other, then any two distinct subspaces from this family are orthogonal.
More concisely: If `V` is a family of orthogonal subspaces of a normed add commutative group `E` over a ring `𝕜`, then any two distinct subspaces `V i` and `V j` are orthogonal to each other.
|
Submodule.isOrtho_bot_left
theorem Submodule.isOrtho_bot_left :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{V : Submodule 𝕜 E}, ⊥.IsOrtho V
This theorem states that for any type `𝕜` and `E`, where `𝕜` is a ring-like structure, `E` is a normed additive commutative group, and an inner product space is defined over `𝕜` and `E`, the zero submodule (denoted as `⊥`) is orthogonal to any given submodule `V` of the inner product space. In other words, in a given inner product space, every element of the zero submodule has an inner product of zero with every element of any other submodule `V`.
More concisely: In an inner product space over a ring-like structure and an additive commutative group, the zero submodule is orthogonal to any given submodule.
|
Submodule.sInf_orthogonal
theorem Submodule.sInf_orthogonal :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(s : Set (Submodule 𝕜 E)), ⨅ K ∈ s, K.orthogonal = (sSup s).orthogonal
This theorem states that for any set 's' of subspaces of a type 'E' in an inner product space over a type '𝕜', the infimum (or greatest lower bound) of the orthogonal complements of the subspaces in 's' is equal to the orthogonal complement of the supremum (or least upper bound) of 's'. The types '𝕜' and 'E' are subject to some conditions: '𝕜' should be a scalar field that supports multiplication and conjugate operation (satisfying the 'RCLike' interface) and 'E' should be a normed additive commutative group which forms an inner product space over '𝕜'.
More concisely: For any set of subspaces of an inner product space over a scalar field with multiplication and conjugate operation, the orthogonal complement of their supremum is equal to the infimum of their orthogonal complements.
|
Submodule.IsOrtho.symm
theorem Submodule.IsOrtho.symm :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{U V : Submodule 𝕜 E}, U.IsOrtho V → V.IsOrtho U
This theorem, "Submodule.IsOrtho.symm", states that for any two submodules `U` and `V` of an inner product space `E` over a ring `𝕜`, if `U` is orthogonal to `V`, then `V` is also orthogonal to `U`. In other words, the orthogonality relation between submodules is symmetric.
More concisely: If submodules U and V of an inner product space E over a ring are orthogonal to each other, then V is orthogonal to U.
|
Submodule.mem_orthogonal'
theorem Submodule.mem_orthogonal' :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(K : Submodule 𝕜 E) (v : E), v ∈ K.orthogonal ↔ ∀ u ∈ K, ⟪v, u⟫_𝕜 = 0
This theorem, `Submodule.mem_orthogonal'`, states that for any given types `𝕜` and `E` where `𝕜` behaves like a ring or a commutative ring and `E` is a normed addition commutative group with associated inner product space, a vector `v` is in the orthogonal complement `Kᗮ` of a submodule `K` if and only if the inner product between `v` and any vector `u` in `K` is zero. This means that `v` is orthogonal to every vector in `K`.
More concisely: A vector `v` is in the orthogonal complement of a submodule `K` in a normed addition commutative group `E` with associated inner product space if and only if the inner product of `v` and every vector `u` in `K` is zero.
|
Submodule.mem_orthogonal_singleton_iff_inner_left
theorem Submodule.mem_orthogonal_singleton_iff_inner_left :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{u v : E}, v ∈ (Submodule.span 𝕜 {u}).orthogonal ↔ ⟪v, u⟫_𝕜 = 0
This theorem states that for any types `𝕜` and `E`, where `𝕜` has a real-like structure (`RCLike 𝕜`) and `E` is a normed add commutative group with an inner product space over `𝕜`, a vector `v` in the orthogonal complement of the span of a singleton set `{u}` (`(Submodule.span 𝕜 {u}).orthogonal`) is orthogonal to `u`. This is equivalent to the statement that the inner product of `v` and `u` is zero, `⟪v, u⟫_𝕜 = 0`. In other words, the vector `v` lies in the orthogonal complement of the span of `u` if and only if `v` is orthogonal to `u`.
More concisely: For any real-like structure `𝕜` and normed add commutative group `E` over `𝕜` with an inner product space structure, a vector `v` in the orthogonal complement of the span of a singleton set `{u}` is orthogonal to `u`, i.e., their inner product is zero (`⟪v, u⟫_𝕜 = 0`).
|
Submodule.orthogonal_gc
theorem Submodule.orthogonal_gc :
∀ (𝕜 : Type u_1) (E : Type u_2) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
GaloisConnection Submodule.orthogonal Submodule.orthogonal
The theorem `Submodule.orthogonal_gc` states that for any scalar type `𝕜`, and any type `E` that forms a normed additive commutative group and an inner product space over `𝕜`, there is a Galois connection between the `Submodule 𝕜 E` and its order dual. This connection is established through the `Submodule.orthogonal` function, which gives the subspace of vectors orthogonal to a given subspace. A Galois connection is a relationship between two functions where the order of elements in the first function's output is the reverse of the order of elements in the second function's output.
More concisely: For any scalar type `𝕜` and normed additive commutative group and inner product space `E` over `𝕜`, there exists a Galois connection between `Submodule 𝕜 E` and its order dual, represented by the `Submodule.orthogonal` function.
|
Submodule.inf_orthogonal_eq_bot
theorem Submodule.inf_orthogonal_eq_bot :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(K : Submodule 𝕜 E), K ⊓ K.orthogonal = ⊥
This theorem states that for a given module `K` over a field `𝕜` in an Inner Product Space of `𝕜` and a Normed Additive Commutative Group `E`, the intersection of `K` and its orthogonal complement `K.orthogonal` is the zero submodule, denoted as `⊥`. In essence, it's asserting that a module and its orthogonal complement have no common elements other than the zero vector.
More concisely: For any inner product space (K, <.>.Over field 𝕜 and normed additive commutative group E), the intersection of K and its orthogonal complement K.orthogonal is equal to the zero submodule. In other words, there are no non-zero common elements between K and K.orthogonal.
|
Submodule.inner_left_of_mem_orthogonal
theorem Submodule.inner_left_of_mem_orthogonal :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{K : Submodule 𝕜 E} {u v : E}, u ∈ K → v ∈ K.orthogonal → ⟪v, u⟫_𝕜 = 0
This theorem states that for any two vectors `u` and `v` in an inner product space over the field `𝕜` with `u` belonging to a submodule `K` of `E` and `v` belonging to the orthogonal complement of `K` (denoted as `K.orthogonal`), the inner product of `v` and `u` equals to zero. This is essentially the mathematical definition of orthogonality in the context of vector spaces: two vectors are orthogonal if their inner product is zero.
More concisely: For any inner product space over field 𝕜, if vector u is in submodule K and vector v is in the orthogonal complement K.orthogonal of K, then u · v = 0. (Here, · represents the inner product.)
|
Submodule.isOrtho_comm
theorem Submodule.isOrtho_comm :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{U V : Submodule 𝕜 E}, U.IsOrtho V ↔ V.IsOrtho U
This theorem states that the orthogonality of submodules in an inner product space is commutative. In more detail, given any field `𝕜`, a normed additively commutative group `E`, and an inner product space structure over `E` with scalars from `𝕜`, for any two submodules `U` and `V` of `E`, `U` is orthogonal to `V` if and only if `V` is orthogonal to `U`. The orthogonal relationship between submodules is symmetric.
More concisely: For any inner product spaces over a commutative field, the orthogonality of submodules is a symmetric relation.
|
Submodule.isClosed_orthogonal
theorem Submodule.isClosed_orthogonal :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(K : Submodule 𝕜 E), IsClosed ↑K.orthogonal
This theorem states that for any given submodule `K` within an Inner Product Space over a field `𝕜` and a Normed Additive Commutative Group `E`, the orthogonal complement of `K` is closed. In other words, given any submodule in the context of inner product spaces, the set of all vectors orthogonal to `K` (denoted as `Kᗮ`) forms a closed set.
More concisely: The orthogonal complement of a submodule in an inner product space is a closed set.
|
OrthogonalFamily.isOrtho
theorem OrthogonalFamily.isOrtho :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{ι : Type u_4} {V : ι → Submodule 𝕜 E},
(OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → ∀ {i j : ι}, i ≠ j → (V i).IsOrtho (V j)
This theorem states that if we have a family of submodules of a normed additive commutative group, which is endowed with an inner product and forms an orthogonal family, then any two submodules in this family with different indices are orthogonal to each other. Here, orthogonality of submodules is understood in the sense of the inner product space. In other words, for any two distinct indices 'i' and 'j', the submodule 'V i' is orthogonal to the submodule 'V j'. This applies to any type of scalar field '𝕜' and any type of index 'ι'.
More concisely: If $\{V\_i\}_{i \in I}$ is a family of orthogonal submodules of a normed additive commutative group endowed with an inner product, then for all distinct indices $i, j \in I$, we have $V\_i \perp V\_j$.
|
Submodule.isOrtho_orthogonal_right
theorem Submodule.isOrtho_orthogonal_right :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
(U : Submodule 𝕜 E), U.IsOrtho U.orthogonal
This theorem states that for any type `𝕜` and any normed additive commutative group `E` with an inner product space over `𝕜`, every submodule `U` of `E` is orthogonal to its orthogonal complement `Uᗮ`. In other words, the inner product of any element of `U` with any element of `Uᗮ` is zero. This theorem is a fundamental property in the field of linear algebra.
More concisely: For any normed additive commutative group `E` with an inner product space over a type `𝕜`, any submodule `U` of `E` is orthogonal to its orthogonal complement `Uᗮ`, i.e., for all `x ∈ U` and `y ∈ Uᗮ`, `∫ x · y = 0`.
|
Submodule.inner_right_of_mem_orthogonal
theorem Submodule.inner_right_of_mem_orthogonal :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{K : Submodule 𝕜 E} {u v : E}, u ∈ K → v ∈ K.orthogonal → ⟪u, v⟫_𝕜 = 0
This theorem states that for any given types `𝕜` (a ring-like structure) and `E` (a normed additive commutative group) where `E` is an inner product space over `𝕜`, and given a submodule `K` of `E`, if a vector `u` is in `K` and another vector `v` is in the orthogonal complement of `K`, then the inner product of `u` and `v` is zero. In other words, `u` and `v` are orthogonal.
More concisely: For any inner product space `(E, ⟨⋅, ⋅⟩)` over a ring `𝕜`, and any submodule `K` of the additive commutative group `E`, if `u ∈ K` and `v ∈ K⊥`, then `⟨u, v⟩ = 0`.
|
OrthogonalFamily.of_pairwise
theorem OrthogonalFamily.of_pairwise :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{ι : Type u_4} {V : ι → Submodule 𝕜 E},
Pairwise ((fun x x_1 => x.IsOrtho x_1) on V) → OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
This theorem, known as `OrthogonalFamily.of_pairwise`, states that for any type `𝕜` with a `RCLike` structure, any normed additive commutative group `E` with an inner product space structure over `𝕜`, any type `ι`, and any function `V` from `ι` into the submodules of `E` over `𝕜`, if the function `V` satisfies the property that for any two distinct elements in the domain `ι`, their corresponding submodules are orthogonal (the `Pairwise` property), then the family of submodules produced by `V` forms an orthogonal family. In the mathematical parlance, if each pair of distinct subspaces in the family `V` are orthogonal, then `V` is an orthogonal family of subspaces.
More concisely: If `V` is a function from a type `ι` into the submodules of a normed additive commutative group `E` over a `RCLike` type `𝕜`, and for all distinct `i, j ∈ ι`, the corresponding submodules `V i` and `V j` are orthogonal, then `V` defines an orthogonal family of subspaces of `E`.
|
Submodule.orthogonal_le
theorem Submodule.orthogonal_le :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{K₁ K₂ : Submodule 𝕜 E}, K₁ ≤ K₂ → K₂.orthogonal ≤ K₁.orthogonal
This theorem, `Submodule.orthogonal_le`, states that for any two subspaces `K₁` and `K₂` of an inner product space `E` over the field `𝕜`, if `K₁` is a subspace of `K₂` (denoted by `K₁ ≤ K₂`), then the orthogonal complement of `K₂` is a subspace of the orthogonal complement of `K₁` (denoted by `K₂.orthogonal ≤ K₁.orthogonal`). This effectively means that the relation `≤` (subset or equals) gets reversed when taking orthogonal complements of subspaces.
More concisely: For any inner product spaces `E` over the field `𝕜` and subspaces `K₁ ≤ K₂` of `E`, `K₁.orthogonal ≤ K₂.orthogonal`.
|
Submodule.orthogonal_orthogonal_monotone
theorem Submodule.orthogonal_orthogonal_monotone :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{K₁ K₂ : Submodule 𝕜 E}, K₁ ≤ K₂ → K₁.orthogonal.orthogonal ≤ K₂.orthogonal.orthogonal
This theorem asserts that the operation `orthogonal.orthogonal` preserves the order `≤` of two subspaces in an inner product space. Specifically, for any two subspaces `K₁` and `K₂` of a given inner product space defined over a field `𝕜` and a normed additive commutative group `E`, if `K₁` is a subspace of `K₂` (`K₁ ≤ K₂`), then the orthogonal complement of the orthogonal complement of `K₁` is also a subspace of the orthogonal complement of the orthogonal complement of `K₂` (`K₁.orthogonal.orthogonal ≤ K₂.orthogonal.orthogonal`).
More concisely: For any inner product spaces K over a field 𝕜 and a normed additive commutative group E, if subspace K₁ is contained in subspace K₂ (K₁ ≤ K₂), then (K₁.orthogonal).orthogonal ≤ (K₂.orthogonal).orthogonal.
|