theorem ContinuousLinearMap.range_eq_top_of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E →L[ℝ] ℝ) (hf : f ≠ 0) : (↑f).range = ⊤

theorem implicit_function_inverse_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (ψ : E → ℝ) (y : E) (Φ : OpenPartialHomeomorph E (ℝ × ↥(↑(fderiv ℝ ψ y)).ker)) {V : Set E} (hV : IsOpen V) (hψ_smooth : ContDiffOn ℝ ⊤ ψ V) (hψ_deriv : fderiv ℝ ψ y ≠ 0) (hy_source : y ∈ Φ.source) (h_source_sub : Φ.source ⊆ V) (h_fwd_smooth : ContDiffOn ℝ ⊤ (↑Φ) Φ.source) : ContDiffOn ℝ ⊤ (↑Φ.symm) Φ.target

theorem implicit_function_straightening {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {V : Set E} (hV : IsOpen V) (ψ : E → ℝ) (y : E) (hy : y ∈ V) (hψ_smooth : ContDiffOn ℝ ⊤ ψ V) (hψ_zero : ψ y = 0) (hψ_deriv : fderiv ℝ ψ y ≠ 0) : ∃ (Φ : OpenPartialHomeomorph E (ℝ × ↥(↑(fderiv ℝ ψ y)).ker)), y ∈ Φ.source ∧ Φ.source ⊆ V ∧ ↑Φ y = (0, 0) ∧ (∀ x ∈ Φ.source, ψ x = (↑Φ x).1) ∧ ContDiffOn ℝ ⊤ (↑Φ) Φ.source ∧ ContDiffOn ℝ ⊤ (↑Φ.symm) Φ.target

theorem implicit_function_diffeomorphism {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {V : Set E} (hV : IsOpen V) (ψ : E → ℝ) (y : E) (hy : y ∈ V) (hψ_smooth : ContDiffOn ℝ ⊤ ψ V) (hψ_zero : ψ y = 0) (hψ_deriv : fderiv ℝ ψ y ≠ 0) : ∃ (Φ : OpenPartialHomeomorph E (ℝ × ↥(↑(fderiv ℝ ψ y)).ker)), y ∈ Φ.source ∧ Φ.source ⊆ V ∧ ↑Φ y = (0, 0) ∧ (∀ x ∈ Φ.source, ψ x = (↑Φ x).1) ∧ ContDiffOn ℝ ⊤ (↑Φ) Φ.source ∧ ContDiffOn ℝ ⊤ (↑Φ.symm) Φ.target

theorem inverse_function_theorem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {φ : E → F} {y : E} (hφ_smooth : ContDiff ℝ ⊤ φ) {f' : E ≃L[ℝ] F} (hf' : HasStrictFDerivAt φ (↑f') y) : ∃ (Φ : OpenPartialHomeomorph E F), (∀ x ∈ Φ.source, ↑Φ x = φ x) ∧ y ∈ Φ.source ∧ IsOpen Φ.source ∧ IsOpen Φ.target ∧ ContDiffOn ℝ ⊤ (↑Φ) Φ.source ∧ ContDiffOn ℝ ⊤ (↑Φ.symm) Φ.target

theorem inverse_function_theorem_local_homeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : E → F) (y : E) (hφ_smooth : ContDiff ℝ ⊤ φ) (f' : E ≃L[ℝ] F) (hf' : HasStrictFDerivAt φ (↑f') y) : ∃ (Φ : OpenPartialHomeomorph E F), (∀ x ∈ Φ.source, ↑Φ x = φ x) ∧ y ∈ Φ.source ∧ IsOpen Φ.source ∧ IsOpen Φ.target ∧ ContDiffOn ℝ ⊤ (↑Φ) Φ.source

structure IsDiffeomorphism {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : E → F) (V : Set E) (U : Set F) : Prop

• isOpen_source : IsOpen V
• isOpen_target : IsOpen U
• bijOn : Set.BijOn φ V U
• smooth_forward : ContDiffOn ℝ ⊤ φ V
• smooth_inverse : ∃ (g : F → E), ContDiffOn ℝ ⊤ g U ∧ (∀ x ∈ V, g (φ x) = x) ∧ ∀ y ∈ U, φ (g y) = y

structure Hypersurface.IsLocalDefiningFunction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ψ : E → ℝ) (M : Set E) (y : E) : Prop

• exists_open_nhd : ∃ (U : Set E), IsOpen U ∧ y ∈ U ∧ ContDiffOn ℝ 1 ψ U ∧ ∀ x ∈ U, x ∈ M ↔ ψ x = 0
• fderiv_ne_zero : fderiv ℝ ψ y ≠ 0

theorem Hypersurface.IsLocalDefiningFunction.differentiableAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ψ : E → ℝ} {M : Set E} {y : E} (hψ : IsLocalDefiningFunction ψ M y) : DifferentiableAt ℝ ψ y

def Hypersurface.IsHypersurface {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : Set E) : Prop

noncomputable def Hypersurface.tangentSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ψ : E → ℝ) (y : E) : Submodule ℝ E

def Hypersurface.IsRegularPoint {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ψ : E → ℝ) (y : E) : Prop

theorem Hypersurface.mem_tangentSpace_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ψ : E → ℝ} {y v : E} : v ∈ tangentSpace ψ y ↔ (fderiv ℝ ψ y) v = 0

theorem Hypersurface.IsLocalDefiningFunction.eq_zero_of_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ψ : E → ℝ} {M : Set E} {y : E} (hψ : IsLocalDefiningFunction ψ M y) (hy : y ∈ M) : ψ y = 0

theorem Hypersurface.IsLocalDefiningFunction.isRegularPoint {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ψ : E → ℝ} {M : Set E} {y : E} (hψ : IsLocalDefiningFunction ψ M y) : IsRegularPoint ψ y

structure Hypersurface.IsSmoothLocalDefiningFunction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ψ : E → ℝ) (M : Set E) (y : E) : Prop

• exists_open_nhd : ∃ (V : Set E), IsOpen V ∧ y ∈ V ∧ ContDiffOn ℝ ⊤ ψ V ∧ (∀ x ∈ V, x ∈ M ↔ ψ x = 0) ∧ ∀ x ∈ V, x ∈ M → fderiv ℝ ψ x ≠ 0

theorem Hypersurface.IsSmoothLocalDefiningFunction.toIsLocalDefiningFunction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ψ : E → ℝ} {M : Set E} {y : E} (hy : y ∈ M) (h : IsSmoothLocalDefiningFunction ψ M y) : IsLocalDefiningFunction ψ M y

theorem Hypersurface.IsSmoothLocalDefiningFunction.eq_zero_of_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ψ : E → ℝ} {M : Set E} {y : E} (hψ : IsSmoothLocalDefiningFunction ψ M y) (hy : y ∈ M) : ψ y = 0

theorem Hypersurface.IsSmoothLocalDefiningFunction.isRegularPoint {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ψ : E → ℝ} {M : Set E} {y : E} (hψ : IsSmoothLocalDefiningFunction ψ M y) (hy : y ∈ M) : IsRegularPoint ψ y

def Hypersurface.IsHypersurfaceSubset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : Set E) : Prop

theorem Hypersurface.smooth_division {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ψ : E → ℝ} {M : Set E} {y : E} (hψ : IsSmoothLocalDefiningFunction ψ M y) (φ : E → ℝ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_vanish : ∃ (V : Set E), IsOpen V ∧ y ∈ V ∧ ∀ x ∈ V, x ∈ M → φ x = 0) : ∃ (W : Set E), IsOpen W ∧ y ∈ W ∧ ∃ (q : E → ℝ), ContDiffOn ℝ ⊤ q W ∧ (∀ x ∈ W, φ x = q x * ψ x) ∧ ∀ (q' : E → ℝ), ContDiffOn ℝ ⊤ q' W → (∀ x ∈ W, φ x = q' x * ψ x) → ∀ x ∈ W, q' x = q x

def Hypersurface.IsConvexHypersurface {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : Set E) : Prop

structure Hypersurface.IsPartialParametrization {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (M : Set E) : Type (max u_1 u_2)

• ambientNhd : Set E
• ambientNhd_open : IsOpen self.ambientNhd
• paramDomain : Set F
• paramDomain_open : IsOpen self.paramDomain
• f : F → E
• smooth : ContDiffOn ℝ ⊤ self.f self.paramDomain
• injective : Set.InjOn self.f self.paramDomain
• image_eq : self.f '' self.paramDomain = M ∩ self.ambientNhd
• immersion (x : F) : x ∈ self.paramDomain → Function.Injective ⇑(fderiv ℝ self.f x)

def Hypersurface.AdmitsPartialParametrization {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : Set E) (y : E) : Prop

theorem Hypersurface.hypersurface_admits_partial_parametrization {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Set E} (hM : IsHypersurfaceSubset M) (y : E) (hy : y ∈ M) : AdmitsPartialParametrization M y

structure Hypersurface.IsGaussMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ν : E → E) (M : Set E) : Prop

• smooth : ContDiffOn ℝ ⊤ ν M
• norm_eq_one (y : E) : y ∈ M → ‖ν y‖ = 1
• orthogonal_tangent (y : E) : y ∈ M → ∀ (ψ : E → ℝ), IsLocalDefiningFunction ψ M y → ∀ v ∈ tangentSpace ψ y, inner ℝ (ν y) v = 0

def Hypersurface.IsOrientable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (M : Set E) : Prop

structure Hypersurface.OrientedHypersurface {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (M : Set E) : Type u_1

• isHypersurface : IsHypersurface M
• gaussMap : E → E
• isGaussMap : IsGaussMap self.gaussMap M

noncomputable def Hypersurface.Curvature.gaussCurvatureMatrix {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ψ : E → ℝ) (y : E) (Y : Fin n → E) (b : OrthonormalBasis (Fin (n + 1)) ℝ E) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

noncomputable def Hypersurface.Curvature.gaussCurvatureLevelSet {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ψ : E → ℝ) (y : E) (Y : Fin n → E) (b : OrthonormalBasis (Fin (n + 1)) ℝ E) : ℝ

noncomputable def Hypersurface.Curvature.shapeOperatorLevelSet {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (ψ : E → ℝ) (y : E) (Y : Fin n → E) : Matrix (Fin n) (Fin n) ℝ

theorem secondFundamentalForm_eq_hessian_div_gradNorm {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (ψ : (Fin (n + 1) → ℝ) → ℝ) (hψ_ne_zero : fderiv ℝ ψ (patch.f x) ≠ 0) (hψ_smooth : ContDiffAt ℝ 2 ψ (patch.f x)) (himage : ∀ u ∈ patch.domain, ψ (patch.f u) = 0) : ∃ (s : ℝ) (_ : s = 1 ∨ s = -1), ∀ (i j : Fin n), secondFundamentalForm patch x i j = s * (((fderiv ℝ (fderiv ℝ ψ) (patch.f x)) (patch.partialDeriv x i)) (patch.partialDeriv x j) / ‖fderiv ℝ ψ (patch.f x)‖)

theorem trace_firstFundamentalForm_inv_mul_eq_sum_orthonormal {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (ψ : (Fin (n + 1) → ℝ) → ℝ) (hψ_ne_zero : fderiv ℝ ψ (patch.f x) ≠ 0) (B : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) → ℝ) (Y : Fin n → Fin (n + 1) → ℝ) (hY_tangent : ∀ (i : Fin n), (fderiv ℝ ψ (patch.f x)) (Y i) = 0) (hY_orthonormal : ∀ (i j : Fin n), ∑ k : Fin (n + 1), Y i k * Y j k = if i = j then 1 else 0) : ((firstFundamentalForm patch x)⁻¹ * Matrix.of fun (i j : Fin n) => B (patch.partialDeriv x i) (patch.partialDeriv x j)).trace = ∑ i : Fin n, B (Y i) (Y i)

theorem meanCurvature_parametric_eq_levelSet {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (ψ : (Fin (n + 1) → ℝ) → ℝ) (hψ_ne_zero : fderiv ℝ ψ (patch.f x) ≠ 0) (hψ_smooth : ContDiffAt ℝ 2 ψ (patch.f x)) (himage : ∀ u ∈ patch.domain, ψ (patch.f u) = 0) (Y : Fin n → Fin (n + 1) → ℝ) (hY_tangent : ∀ (i : Fin n), (fderiv ℝ ψ (patch.f x)) (Y i) = 0) (hY_orthonormal : ∀ (i j : Fin n), ∑ k : Fin (n + 1), Y i k * Y j k = if i = j then 1 else 0) : ∃ (s : ℝ) (_ : s = 1 ∨ s = -1), meanCurvature patch x = s * (1 / ‖fderiv ℝ ψ (patch.f x)‖ * ∑ i : Fin n, ((fderiv ℝ (fderiv ℝ ψ) (patch.f x)) (Y i)) (Y i))

structure Hypersurface.IsTangentCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ → E) (M : Set E) (y v : E) : Prop

• at_zero : c 0 = y
• hasDerivAt : HasDerivAt c v 0
• image_in_M : ∀ᶠ (t : ℝ) in nhds 0, c t ∈ M

theorem Hypersurface.tangent_of_curve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ψ : E → ℝ} {M : Set E} {y v : E} {c : ℝ → E} (hψ : IsLocalDefiningFunction ψ M y) (hc : IsTangentCurve c M y v) : v ∈ tangentSpace ψ y

theorem Hypersurface.curve_of_tangent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ψ : E → ℝ} {M : Set E} {y v : E} (hψ : IsLocalDefiningFunction ψ M y) (hy : y ∈ M) (hv : v ∈ tangentSpace ψ y) (hstrict : HasStrictFDerivAt ψ (fderiv ℝ ψ y) y) : ∃ (c : ℝ → E), IsTangentCurve c M y v