Closed interval to 0-manifolds are discrete spaces

TheoremClosed interval#

The manifold structure on [x, y] is smooth.

instIsManifoldIcc (x y : ℝ) [Fact (x < y)] {n : WithTop ℕ∞} :
  IsManifold (modelWithCornersEuclideanHalfSpace 1) n ↑(Set.Icc x y)

Sources

• Mathlib documentation: instIsManifoldIcc
• Source of instIsManifoldIcc in Mathlib/Geometry/Manifold/Instances/Real.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibinstIsManifoldIcc

Uses 7

Statement usesInner product space, over \(R\) or \(C\) · Norms \(\lVert\cdot\rVert_p\) on \(\R^n\) and \(\C^n\) · Smooth or analytic manifold (with boundary and corners)

Proof uses\(C^k\) function · Ordered ring · The Triangle Inequality · Topological ring

TheoremGeneral linear group as a Lie group#

The units of a complete normed ring form a Lie group.

Units.instLieGroupModelWithCornersSelf.{u_1, u_2} {R : Type u_1} [NormedRing R] [CompleteSpace R]
  {n : WithTop ℕ∞} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 R] :
  LieGroup (modelWithCornersSelf 𝕜 R) n Rˣ

Sources

• Mathlib documentation: Units.instLieGroupModelWithCornersSelf
• Source of Units.instLieGroupModelWithCornersSelf in Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibUnits.instLieGroupModelWithCornersSelf

Uses 6

Statement usesLie group

Proof uses\(C^k\) function · Induced topology · Invertible elements · Open map · Topology of a metric space

TheoremDiscrete spaces are 0-manifolds#

A discrete space M is a smooth manifold over the trivial model on a trivial normed space.

IsManifold.of_discreteTopology.{u_1, u_2, u_4} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (n : WithTop ℕ∞) {M : Type u_4}
  [TopologicalSpace M] [DiscreteTopology M] [Unique E] : IsManifold (modelWithCornersSelf 𝕜 E) n M

Sources

• Mathlib documentation: IsManifold.of_discreteTopology
• Source of IsManifold.of_discreteTopology in Mathlib/Geometry/Manifold/IsManifold/Basic.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibIsManifold.of_discreteTopology

Uses 2

Statement usesSmooth or analytic manifold (with boundary and corners)

Proof uses\(C^k\) function

Theorem0-manifolds are discrete spaces#

A charted space over a discrete space is discrete.

ChartedSpace.discreteTopology.{u, u_2} (H : Type u) (M : Type u_2) [TopologicalSpace H]
  [TopologicalSpace M] [ChartedSpace H M] [DiscreteTopology H] : DiscreteTopology M

Sources

• Mathlib documentation: ChartedSpace.discreteTopology
• Source of ChartedSpace.discreteTopology in Mathlib/Geometry/Manifold/ChartedSpace.lean
• Mathlib overview: Geometry › Differentiable manifolds

MathlibChartedSpace.discreteTopology

Uses 2

Statement usesLimit of a map with respect to filters · Topological space

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.