-
Notifications
You must be signed in to change notification settings - Fork 314
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: port Analysis.Calculus.AffineMap (#4893)
- Loading branch information
1 parent
697b395
commit 1cad7fe
Showing
2 changed files
with
43 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,42 @@ | ||
/- | ||
Copyright (c) 2021 Oliver Nash. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Oliver Nash | ||
! This file was ported from Lean 3 source module analysis.calculus.affine_map | ||
! leanprover-community/mathlib commit 839b92fedff9981cf3fe1c1f623e04b0d127f57c | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
-/ | ||
import Mathlib.Analysis.NormedSpace.ContinuousAffineMap | ||
import Mathlib.Analysis.Calculus.ContDiff | ||
|
||
/-! | ||
# Smooth affine maps | ||
This file contains results about smoothness of affine maps. | ||
## Main definitions: | ||
* `ContinuousAffineMap.contDiff`: a continuous affine map is smooth | ||
-/ | ||
|
||
|
||
namespace ContinuousAffineMap | ||
|
||
variable {π V W : Type _} [NontriviallyNormedField π] | ||
|
||
variable [NormedAddCommGroup V] [NormedSpace π V] | ||
|
||
variable [NormedAddCommGroup W] [NormedSpace π W] | ||
|
||
/-- A continuous affine map between normed vector spaces is smooth. -/ | ||
theorem contDiff {n : ββ} (f : V βA[π] W) : ContDiff π n f := by | ||
rw [f.decomp] | ||
apply f.contLinear.contDiff.add | ||
simp only | ||
exact contDiff_const | ||
#align continuous_affine_map.cont_diff ContinuousAffineMap.contDiff | ||
|
||
end ContinuousAffineMap |