JacobsonSpace

📁 Source: Mathlib/Topology/JacobsonSpace.lean

Statistics

Metric	Count
Definitions JacobsonSpace, closedPoints	2
Theorems closure_inter_closedPoints, closure_inter_closedPoints_eq_closure, discreteTopology, of_isClosedEmbedding, of_isOpenEmbedding, isDiscrete_of_subset_closedPoints, jacobsonSpace_iff, preimage_closedPoints, preimage_closedPoints, closedPoints_eq_univ, closure_closedPoints, instDiscreteTopologyOfFiniteOfJacobsonSpace, instJacobsonSpaceOfT1Space, isClosed_singleton_of_isLocallyClosed_singleton, jacobsonSpace_iff, jacobsonSpace_iff_locallyClosed, mem_closedPoints_iff, nonempty_inter_closedPoints, preimage_closedPoints_subset, subsingleton_image_closure_of_finite_of_isPreirreducible	20
Total	22

JacobsonSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_inter_closedPoints 📖	mathematical	—	closure Set Set.instInter closedPoints	—	—
closure_inter_closedPoints_eq_closure 📖	mathematical	IsLocallyClosed	closure Set Set.instInter closedPoints	—	HasSubset.Subset.antisymm Set.instAntisymmSubset closure_mono Set.inter_subset_left IsClosed.closure_subset_iff isClosed_closure nonempty_inter_closedPoints IsLocallyClosed.inter IsOpen.isLocallyClosed IsClosed.isOpen_compl subset_closure
discreteTopology 📖	mathematical	—	DiscreteTopology	—	Set.univ_subset_iff closure_closedPoints closure_subset_iff_isClosed Set.biUnion_of_singleton Set.Finite.isClosed_biUnion Set.finite_univ_iff discreteTopology_iff_forall_isOpen isClosed_compl_iff Set.toFinite Subtype.finite mem_closedPoints_iff
of_isClosedEmbedding 📖	mathematical	Topology.IsClosedEmbedding	JacobsonSpace	—	jacobsonSpace_iff_locallyClosed Topology.IsClosedEmbedding.preimage_closedPoints nonempty_inter_closedPoints Set.Nonempty.image IsLocallyClosed.image Topology.IsClosedEmbedding.isInducing IsClosed.isLocallyClosed Topology.IsClosedEmbedding.isClosed_range
of_isOpenEmbedding 📖	mathematical	Topology.IsOpenEmbedding	JacobsonSpace	—	jacobsonSpace_iff_locallyClosed Topology.IsOpenEmbedding.preimage_closedPoints nonempty_inter_closedPoints Set.Nonempty.image IsLocallyClosed.image Topology.IsOpenEmbedding.isInducing IsOpen.isLocallyClosed Topology.IsOpenEmbedding.isOpen_range

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDiscrete_of_subset_closedPoints 📖	mathematical	Set Set.instHasSubset closedPoints	IsDiscrete	—	Set.ext IsClosed.preimage continuous_subtype_val Finite.instDiscreteTopology

TopologicalSpace.IsOpenCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
jacobsonSpace_iff 📖	mathematical	TopologicalSpace.IsOpenCover	JacobsonSpace TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype	—	JacobsonSpace.of_isOpenEmbedding IsOpen.isOpenEmbedding_subtypeVal TopologicalSpace.Opens.is_open' jacobsonSpace_iff_locallyClosed Set.nonempty_iUnion iUnion_inter IsLocallyClosed.preimage continuous_subtype_val isClosed_iff_coe_preimage Set.ext isClosed_singleton_of_isLocallyClosed_singleton Set.image_singleton IsLocallyClosed.image IsClosed.isLocallyClosed Topology.IsEmbedding.isInducing Topology.IsEmbedding.subtypeVal IsOpen.isLocallyClosed Topology.IsOpenEmbedding.isOpen_range Set.eq_empty_iff_forall_notMem isClosed_empty

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preimage_closedPoints 📖	mathematical	Topology.IsClosedEmbedding	Set.preimage closedPoints	—	Set.ext isClosed_iff_image_isClosed

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preimage_closedPoints 📖	mathematical	Topology.IsOpenEmbedding	Set.preimage closedPoints	—	subset_antisymm Set.instAntisymmSubset preimage_closedPoints_subset Topology.IsEmbedding.injective toIsEmbedding continuous isClosed_singleton_of_isLocallyClosed_singleton Set.image_singleton IsLocallyClosed.image IsClosed.isLocallyClosed isInducing IsOpen.isLocallyClosed isOpen_range

(root)

Definitions

Name	Category	Theorems
JacobsonSpace 📖	CompData	12 math math: JacobsonSpace.of_isOpenEmbedding, jacobsonSpace_iff, jacobsonSpace_iff_locallyClosed, TopologicalSpace.IsOpenCover.jacobsonSpace_iff, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing, instJacobsonSpaceOfT1Space, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier, JacobsonSpace.of_isClosedEmbedding, AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace, PrimeSpectrum.instJacobsonSpaceOfIsJacobsonRing, PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace
closedPoints 📖	CompOp	14 math math: AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints, JacobsonSpace.closure_inter_closedPoints, nonempty_inter_closedPoints, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, jacobsonSpace_iff, jacobsonSpace_iff_locallyClosed, Topology.IsClosedEmbedding.preimage_closedPoints, closure_closedPoints, preimage_closedPoints_subset, closedPoints_eq_univ, JacobsonSpace.closure_inter_closedPoints_eq_closure, Topology.IsOpenEmbedding.preimage_closedPoints, AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe, mem_closedPoints_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedPoints_eq_univ 📖	mathematical	—	closedPoints Set.univ	—	Set.eq_univ_iff_forall isClosed_singleton
closure_closedPoints 📖	mathematical	—	closure closedPoints Set.univ	—	Set.univ_inter JacobsonSpace.closure_inter_closedPoints isClosed_univ
instDiscreteTopologyOfFiniteOfJacobsonSpace 📖	mathematical	—	DiscreteTopology	—	JacobsonSpace.discreteTopology Set.toFinite Subtype.finite
instJacobsonSpaceOfT1Space 📖	mathematical	—	JacobsonSpace	—	closedPoints_eq_univ Set.inter_univ
isClosed_singleton_of_isLocallyClosed_singleton 📖	mathematical	IsLocallyClosed Set Set.instSingletonSet	IsClosed	—	nonempty_inter_closedPoints Set.singleton_nonempty
jacobsonSpace_iff 📖	mathematical	—	JacobsonSpace closure Set Set.instInter closedPoints	—	—
jacobsonSpace_iff_locallyClosed 📖	mathematical	—	JacobsonSpace Set.Nonempty Set Set.instInter closedPoints	—	jacobsonSpace_iff HasSubset.Subset.trans Set.instIsTransSubset subset_closure isClosed_closure IsClosed.closure_subset_iff Set.subset_diff Set.disjoint_iff Set.inter_assoc Set.inter_comm Set.inter_subset_left Set.inter_subset_right Set.bot_eq_empty disjoint_self subset_antisymm Set.instAntisymmSubset Set.disjoint_compl_left_iff_subset Set.disjoint_iff_inter_eq_empty Set.not_nonempty_iff_eq_empty IsLocallyClosed.inter IsOpen.isLocallyClosed IsClosed.isOpen_compl IsClosed.isLocallyClosed Set.nonempty_iff_ne_empty
mem_closedPoints_iff 📖	mathematical	—	Set Set.instMembership closedPoints IsClosed Set.instSingletonSet	—	—
nonempty_inter_closedPoints 📖	mathematical	Set.Nonempty IsLocallyClosed	Set Set.instInter closedPoints	—	jacobsonSpace_iff_locallyClosed
preimage_closedPoints_subset 📖	mathematical	Continuous	Set Set.instHasSubset Set.preimage closedPoints	—	mem_closedPoints_iff Set.image_singleton Set.preimage_image_eq continuous_iff_isClosed
subsingleton_image_closure_of_finite_of_isPreirreducible 📖	mathematical	IsLocallyClosed IsPreirreducible Continuous IsClosedMap	Set.Subsingleton Set.image closure	—	Set.eq_empty_or_nonempty IsClosed.closure_eq Set.image_empty isIrreducible_iff_closure JacobsonSpace.closure_inter_closedPoints_eq_closure Set.image_singleton IsDiscrete.subsingleton_of_isPreirreducible Set.Finite.isDiscrete_of_subset_closedPoints Set.Finite.subset Set.image_mono Set.inter_subset_left IsIrreducible.isPreirreducible IsIrreducible.image Continuous.continuousOn Set.Subsingleton.eq_singleton_of_mem image_closure_subset_closure_image Set.Subsingleton.anti

---

← Back to Index