Library mathcomp.analysis.prodnormedzmodule
This file equips the product of two normedZmodTypes with a canonical
normedZmodType structure. It is a short file that has been added here for
convenience during the rebase of MathComp-Analysis on top of MathComp 1.1.
The contents is likely to be moved elsewhere.
Set Implicit Arguments.
Local Open Scope ring_scope.
Import Order.TTheory GRing.Theory Num.Theory.
Module ProdNormedZmodule.
Section ProdNormedZmodule.
Context {R : numDomainType} {U V : normedZmodType R}.
Definition norm (x : U × V) : R := Num.max `|x.1| `|x.2|.
Lemma normD x y : norm (x + y) ≤ norm x + norm y.
Lemma norm_eq0 x : norm x = 0 → x = 0.
Lemma normMn x n : norm (x *+ n) = (norm x) *+ n.
Lemma normrN x : norm (- x) = norm x.
Definition normedZmodMixin :
@Num.normed_mixin_of R [zmodType of U × V] (Num.NumDomain.class R) :=
@Num.NormedMixin _ _ _ norm normD norm_eq0 normMn normrN.
Canonical normedZmodType := NormedZmodType R (U × V) normedZmodMixin.
Lemma prod_normE (x : normedZmodType) : `|x| = Num.max `|x.1| `|x.2|.
End ProdNormedZmodule.
Module Exports.
Canonical normedZmodType.
Definition prod_normE := @prod_normE.
End Exports.
End ProdNormedZmodule.
Export ProdNormedZmodule.Exports.