Mathlib Map

Theorems · Theorem · general topology

isClosed_empty

∀ {X : Type u} [inst : TopologicalSpace X], IsClosed ∅
Defined in
Mathlib.Topology.Basic
Cited by
26 results in Mathlib
Foundations
Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

exists_continuous_nonneg_pos · cited by 15exists_continuous_nonneg_…closure_empty · cited by 11closure_emptyFilter.hasBasis_coclosedCompact · cited by 8Filter.hasBasis_coclosedC…Set.Subsingleton.isClosed · cited by 3Subsingleton.isClosedUniformSpace.hausdorff.isClopen_singleton_empty · cited by 2hausdorff.isClopen_single…TopologicalSpace.vietoris.isClopen_singleton_empty · cited by 2vietoris.isClopen_singlet…MeasurableSet.exists_isClosed_lt_add · cited by 2MeasurableSet.exists_isCl…isClosedMap_sigmaMk · cited by 2isClosedMap_sigmaMkhasBasis_coclosedLindelof · cited by 2hasBasis_coclosedLindelofIsLowerSet.isClosed · cited by 1IsLowerSet.isClosedTopologicalSpace.IsOpenCover.jacobsonSpace_iff · cited by 1IsOpenCover.jacobsonSpace…Order.IsNormal.continuous · cited by 1IsNormal.continuousMeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite · cited by 1InnerRegularWRT.weaklyReg…Continuous.exists_contDiff_approx · cited by 1Continuous.exists_contDif…Topology.RelCWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell · cited by 1RelCWComplex.isClosed_of_…Set · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpaceIsClosed · cited by 1639IsClosedisClosed_const · cited by 3isClosed_constisClosed_emptyCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by26

Results whose statement or proof uses this declaration.