Revision #2365 → #2538 · back to history
modifiedHeine–Borel theorem (lead)204e0f88f209
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | isCompact_iff_isClosed_bounded | Metric.isCompact_iff_isClosed_bounded |
| provenance | ai | ai-moderated |
modifiedHeine–Borel lemmad772338dfef8
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | isCompact_iff_isClosed_bounded | Metric.isCompact_iff_isClosed_bounded |
| provenance | ai | ai-moderated |
modifiedUnit interval is compactc35bbc2e9c6a
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | isCompact_Icc | CompactIccSpace.isCompact_Icc |
| provenance | ai | ai-moderated |
modifiedHalf-line [0,∞) not compact5c9f3009ea62
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | Real.noncompactSpace | RealNormedSpace.noncompactSpace |
| provenance | ai | ai-moderated |
modifiedClosed disks and circles compact; open disk not38272fc62789
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | isCompact_closedBall | ProperSpace.isCompact_closedBall |
| provenance | ai | ai-moderated |
modifiedCompactness in Euclidean spacea0bc97788b41
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | isCompact_iff_isClosed_bounded | Metric.isCompact_iff_isClosed_bounded |
| provenance | ai | ai-moderated |
modifiedHeine–Borel theorem84c6c900df21
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | isCompact_iff_isClosed_bounded | Metric.isCompact_iff_isClosed_bounded |
| provenance | ai | ai-moderated |
modifiedCompact metric space is second-countable, separable, Lindelöfc1badaa52f91
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | TopologicalSpace.SecondCountableTopology | SecondCountableTopology |
| provenance | ai | ai-moderated |
modifiedEvaluation map is a ring homomorphism3add53ccfb9b
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | ContinuousMap.evalRingHom | ContinuousMap.evalAlgHom |
| provenance | ai | ai-moderated |
modifiedDiscrete spaces and compactness134dcbb63300
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | DiscreteTopology.compactSpace_iff_finite | finite_of_compact_of_discrete |
| provenance | ai | ai-moderated |
modified[0,1] compact, (0,1) not, rationals in [0,1] not4657a8e5fb6f
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | isCompact_Icc | CompactIccSpace.isCompact_Icc |
| provenance | ai | ai-moderated |
modifiedReal line not compactbf2136bad1e5
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | Real.noncompactSpace | RealNormedSpace.noncompactSpace |
| provenance | ai | ai-moderated |
modifiedProkhorov's theorem8397966eeb4f
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | MeasureTheory.IsTightMeasureSet.isCompact_closure | isCompact_closure_of_isTightMeasureSet |
| provenance | ai | ai-moderated |
modifiedStructure space of Banach algebra compact80f114d79f93
| Field | From #2365 | To #2538 |
|---|
| mathlib.decl | WeakDual.CharacterSpace.instCompactSpace | WeakDual.CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace |
| provenance | ai | ai-moderated |