IsLprojection.coe_sup
theorem IsLprojection.coe_sup :
โ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
[inst_3 : FaithfulSMul M X] (P Q : { P // IsLprojection X P }), โ(P โ Q) = โP + โQ - โP * โQ
This theorem states that for any normed commutative add group `X` and any ring `M` that is also a module over `X`, given the condition that scalar multiplication by `M` on `X` is faithful, for any two elements `P` and `Q` of the set of `P` such that `P` is a left-projection on `X`, the supremum of `P` and `Q` is equal to `P` plus `Q` minus the product of `P` and `Q`.
More concisely: Given a normed commutative add group `X` and an associative ring `M` making `X` a left `M`-module with faithful scalar multiplication, for any left-projection `P` in `X`, we have $P + Q - PQ = \sup(P, Q)$.
|
IsLprojection.Lcomplement
theorem IsLprojection.Lcomplement :
โ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] {P : M},
IsLprojection X P โ IsLprojection X (1 - P)
This theorem states that for any type `X` which is a Normed Additive Commutative Group, and any type `M` which is a Ring and a Module over `X`, and any element `P` of `M`, if `P` is a left projection on `X`, then `1 - P` is also a left projection on `X`. In mathematical terms, we can say that if a linear map `P` is a projection on a vector space `X`, then `1 - P` (where `1` here represents the identity operator on `X`) is also a projection on `X`.
More concisely: If `P` is a left projection on the normed additive commutative group `X` as a module over the ring `M`, then `1 - P` is also a left projection on `X`.
|
IsLprojection.coe_inf
theorem IsLprojection.coe_inf :
โ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
[inst_3 : FaithfulSMul M X] (P Q : { P // IsLprojection X P }), โ(P โ Q) = โP * โQ
This theorem, `IsLprojection.coe_inf`, states that for any type `X` that is a Normed Additive Commutative Group, any type `M` that is a Ring and also a Module over `X`, and given `M` and `X` satisfy the Faithful Scalar Multiplication property, for any two elements `P` and `Q` in the set of elements that satisfy the Left projection property over `X`, the meet operation (infimum, denoted by `โ`) of `P` and `Q` is equal to the scalar multiple of `P` and `Q`. In other words, the left projection of `P` and `Q` is the same as multiplying the individual left projections of `P` and `Q`.
More concisely: For any Normed Additive Commutative Group `X`, Ring `M` that is a Module over `X` with the Faithful Scalar Multiplication property, the infimum of two elements `P` and `Q` in `X` that satisfy the Left projection property is equal to the scalar multiple of their individual left projections.
|
IsLprojection.mul
theorem IsLprojection.mul :
โ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
[inst_3 : FaithfulSMul M X] {P Q : M}, IsLprojection X P โ IsLprojection X Q โ IsLprojection X (P * Q)
This theorem states that for any types `X` and `M`, where `X` is a normed add commutative group and `M` is a ring, and `X` is a module over `M` with faithful scalar multiplication, if `P` and `Q` are elements of `M` that are left projections onto `X`, then the product `P * Q` is also a left projection onto `X`. A left projection in this context is an idempotent linear transformation from the module to itself.
More concisely: If `X` is a normed add commutative group and a faithful `M`-module, where `M` is a ring, and `P` and `Q` are left projections in `M` onto `X`, then `P * Q` is also a left projection onto `X`.
|
IsLprojection.coe_compl
theorem IsLprojection.coe_compl :
โ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
(P : { P // IsLprojection X P }), โPแถ = 1 - โP
The theorem `IsLprojection.coe_compl` states that for any type `X` that forms a Normed Additive Commutative Group, any type `M` that forms a Ring and a Module over `X`, and for any `P` that is a left projection in `X`, the complement of `P` is equal to `1 - P`. In simpler terms, it's saying that if we have a certain mathematical structure (the left projection `P`), then the complement of this structure is simply one minus the structure itself.
More concisely: For any Normed Additive Commutative Group `X`, Ring `M`, and Module `M` over `X`, if `P` is a left projection in `X`, then `1 - P` is the complement of `P`.
|
IsLprojection.le_def
theorem IsLprojection.le_def :
โ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
[inst_3 : FaithfulSMul M X] (P Q : { P // IsLprojection X P }), P โค Q โ โP = โ(P โ Q)
This theorem describes a property of left (L-) projections in the context of normed additive commutative groups and modules over a ring. Specifically, for any two left projections 'P' and 'Q', 'P' is less than or equal to 'Q' if and only if 'P' equals the infimum of 'P' and 'Q'. This theorem essentially sets a condition for the partial ordering of left projections in a mathematical structure where scalar multiplication is faithful.
More concisely: For left projections P and Q in the context of normed additive commutative groups and modules over a ring, P โค Q if and only if P = inf(P, Q).
|