Library mathcomp.analysis.prodnormedzmodule
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import div fintype path bigop order finset fingroup.
From mathcomp Require Import ssralg poly ssrnum.
Require Import nngnum.
From mathcomp Require Import div fintype path bigop order finset fingroup.
From mathcomp Require Import ssralg poly ssrnum.
Require Import nngnum.
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.