Revision #1477 → #2145 · back to history
modifiedPoint (geometry)9bfab7e06a9c
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | An informal abstract idealization, not a single Mathlib declaration; Mathlib uses elements of various spaces (sets, affine spaces, etc.) but has no overarching `Point` definition. |
| status | — | not_formalized |
modifiedPoint as primitive notion50f1c83a09ac
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Philosophical/Euclidean primitive notion with no direct Mathlib counterpart. |
| status | — | not_formalized |
modifiedVertex / cornerb19fed792bf2
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No general intersection-vertex/corner definition exists in Mathlib at this informal level. |
| status | — | not_formalized |
addedPoint set19dce82a9e7f
modifiedIsolated pointbcb87c0b99bb
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | PerfectSpace.not_isolated |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Topology.Perfect |
| note | — | Mathlib expresses isolation via `Filter.NeBot (𝓝[≠] x)` (perfect-space context) rather than a standalone `IsIsolatedPoint` predicate. |
| status | — | partial |
modifiedPoint in the Euclidean planea594aff141b5
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | EuclideanSpace |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Analysis.InnerProductSpace.PiL2 |
| note | — | Points in the Euclidean plane are elements of `EuclideanSpace ℝ (Fin 2)`. |
| status | — | formalized |
modifiedPoint in n-dimensional space5e2556077994
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | EuclideanSpace |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.InnerProductSpace.PiL2 |
| note | — | `EuclideanSpace 𝕜 (Fin n)` realizes points as ordered n-tuples. |
| status | — | formalized |
modifiedLine as a set of pointsa29ffb0cdc15
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | AffineSubspace |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs |
| note | — | Mathlib formalizes lines as one-dimensional affine subspaces (a special case of `AffineSubspace`). |
| status | — | formalized |
modifiedDegenerate line segment086329903ab9
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `DegenerateSegment` predicate; degenerate segments are not given a dedicated name in Mathlib. |
| status | — | not_formalized |
modifiedTwo points determine a lineb75be0476504
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | AffineSubspace.affineSpan_pair |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs |
| note | — | Mathlib has `affineSpan` of two points but no single canonical statement equivalent to Euclid's `two points determine a line` axiom. |
| status | — | partial |
modifiedPoint is 0-dimensional2f760b3b34ab
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | dimH_singleton |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Topology.MetricSpace.HausdorffDimension |
| note | — | Mathlib proves dimension zero for a point under the Hausdorff-dimension and rank notions, but not a single unified `point is 0-dimensional` statement covering all dimension theories. |
| status | — | partial |
modifiedVector space dimensionf48553117597
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | Module.rank |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.LinearAlgebra.Dimension.Basic |
| note | — | `Module.rank` (and its finite cousin `Module.finrank`) is the dimension of a module/vector space. |
| status | — | formalized |
modifiedSingle-point vector space has no linearly independent subsetb85b75a2130d
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | rank_subsingleton' |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.LinearAlgebra.Dimension.Subsingleton |
| note | — | `rank_subsingleton'` proves `Module.rank R M = 0` whenever `M` is subsingleton, e.g. the trivial vector space. |
| status | — | formalized |
modifiedTopological (covering) dimensionf4e49e335c37
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Lebesgue covering dimension is not defined in Mathlib (no `topologicalDimension`/`coveringDimension`). |
| status | — | not_formalized |
addedInfinite covering dimensionfddc6f5e9a50
modifiedPoint has covering dimension zero09e4a691b0a3
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No covering dimension is defined in Mathlib, so this statement is not stated there. |
| status | — | not_formalized |
modifiedHausdorff contentb77ab4a23442
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | MeasureTheory.Measure.hausdorffMeasure |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.MeasureTheory.Measure.Hausdorff |
| note | — | Mathlib defines the Hausdorff measure `μH[d]` (built via `mkMetric`); the unrestricted-diameter Hausdorff content is not separately named. |
| status | — | partial |
modifiedHausdorff dimension1b6e6529e88a
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | dimH |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.MetricSpace.HausdorffDimension |
| note | — | `dimH` is the Hausdorff dimension of a set in a (pseudo-)e-metric space. |
| status | — | formalized |
modifiedPoint has Hausdorff dimension 05ca2ad208d83
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | dimH_singleton |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.MetricSpace.HausdorffDimension |
| note | — | `dimH_singleton` states `dimH {x} = 0`. |
| status | — | formalized |
modifiedPointless spacefd7d733d3660
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has frames/locales-adjacent material (e.g. `Order.Frame`) but no `Pointless`/`Pointfree` space construct as a standalone concept. |
| status | — | not_formalized |
modifiedDirac delta functionfd7930228bc9
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | MeasureTheory.Measure.dirac |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.MeasureTheory.Measure.Dirac |
| note | — | Mathlib formalizes the Dirac delta as the Dirac measure `Measure.dirac a` (and as a tempered distribution in `Analysis.Distribution.TemperedDistribution`). |
| status | — | formalized |
modifiedKronecker delta function96350f6d36b5
| Field | From #1477 | To #2145 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has Kronecker matrix products but no dedicated `kroneckerDelta` function; uses `if i = j then 1 else 0` (e.g. via `Matrix.one_apply`) ad hoc. |
| status | — | not_formalized |