From d0507e7be36876e9e2c84a710de50346ef187fd4 Mon Sep 17 00:00:00 2001 From: Joseph Myers Date: Fri, 23 Sep 2022 08:22:36 +0000 Subject: [PATCH] =?UTF-8?q?feat(analysis/normed=5Fspace/affine=5Fisometry)?= =?UTF-8?q?:=20`subtype=E2=82=90=E1=B5=A2`=20(#16573)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Now that we have `affine_subspace.subtype`, add the corresponding definition as a bundled affine isometry (so resolving a comment about that being missing). The name uses subscript `ₐᵢ` rather than superscript `ᵃⁱ` as in the notation for `affine_isometry` because Lean does not accept the superscript in identifiers. --- .../normed_space/affine_isometry.lean | 28 +++++++++++++++++-- 1 file changed, 25 insertions(+), 3 deletions(-) diff --git a/src/analysis/normed_space/affine_isometry.lean b/src/analysis/normed_space/affine_isometry.lean index 269c09455175d..838114494fa23 100644 --- a/src/analysis/normed_space/affine_isometry.lean +++ b/src/analysis/normed_space/affine_isometry.lean @@ -197,9 +197,31 @@ instance : monoid (P →ᵃⁱ[𝕜] P) := end affine_isometry --- remark: by analogy with the `linear_isometry` file from which this is adapted, there should --- follow here a section defining an "inclusion" affine isometry from `p : affine_subspace 𝕜 P` --- into `P`; we omit this for now +namespace affine_subspace + +include V + +/-- `affine_subspace.subtype` as an `affine_isometry`. -/ +def subtypeₐᵢ (s : affine_subspace 𝕜 P) [nonempty s] : s →ᵃⁱ[𝕜] P := +{ norm_map := s.direction.subtypeₗᵢ.norm_map, + .. s.subtype } + +lemma subtypeₐᵢ_linear (s : affine_subspace 𝕜 P) [nonempty s] : + s.subtypeₐᵢ.linear = s.direction.subtype := +rfl + +@[simp] lemma subtypeₐᵢ_linear_isometry (s : affine_subspace 𝕜 P) [nonempty s] : + s.subtypeₐᵢ.linear_isometry = s.direction.subtypeₗᵢ := +rfl + +@[simp] lemma coe_subtypeₐᵢ (s : affine_subspace 𝕜 P) [nonempty s] : ⇑s.subtypeₐᵢ = s.subtype := +rfl + +@[simp] lemma subtypeₐᵢ_to_affine_map (s : affine_subspace 𝕜 P) [nonempty s] : + s.subtypeₐᵢ.to_affine_map = s.subtype := +rfl + +end affine_subspace variables (𝕜 P P₂) include V V₂