Documentation Verification Report

Sober

📁 Source: Mathlib/Topology/Sober.lean

Statistics

Metric	Count
Definitions `IsGenericPoint`, `genericPoint`, `QuasiSober`, `genericPoint`, `genericPoints`, `component`, `equiv`, `ofComponent`, `irreducibleSetEquivPoints`	9
Theorems `def`, `disjoint_iff`, `eq`, `image`, `inseparable`, `isClosed`, `isIrreducible`, `mem`, `mem_closed_set_iff`, `mem_open_set_iff`, `specializes`, `specializes_iff_mem`, `closure_genericPoint`, `genericPoint_closure_eq`, `isGenericPoint_genericPoint`, `isGenericPoint_genericPoint_closure`, `sober`, `quasiSober`, `quasiSober`, `quasiSober_iff_forall`, `quasiSober`, `quasiSober`, `genericPoint_closure`, `genericPoint_spec`, `genericPoint_specializes`, `closure`, `component_injective`, `component_ofComponent`, `component_surjective`, `equiv_apply`, `equiv_symm_apply`, `finite`, `isGenericPoint`, `isGenericPoint_ofComponent`, `ofComponent_component`, `genericPoints_eq_singleton`, `isGenericPoint_closure`, `isGenericPoint_def`, `isGenericPoint_iff_forall_closed`, `isGenericPoint_iff_specializes`, `quasiSober_iff`, `quasiSober_of_open_cover`	42
Total	51

IsGenericPoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`def` 📖	mathematical	`IsGenericPoint`	`closure` `Set` `Set.instSingletonSet`	—	—
`disjoint_iff` 📖	mathematical	`IsGenericPoint` `IsOpen`	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instMembership`	—	`mem_open_set_iff` `Set.not_disjoint_iff_nonempty_inter`
`eq` 📖	—	`IsGenericPoint`	—	—	`Inseparable.eq` `inseparable`
`image` 📖	mathematical	`IsGenericPoint` `Continuous`	`closure` `Set.image`	—	`isGenericPoint_def` `def` `Set.image_singleton` `closure_image_closure`
`inseparable` 📖	mathematical	`IsGenericPoint`	`Inseparable`	—	`Specializes.antisymm` `specializes` `mem`
`isClosed` 📖	mathematical	`IsGenericPoint`	`IsClosed`	—	`isClosed_closure` `def`
`isIrreducible` 📖	mathematical	`IsGenericPoint`	`IsIrreducible`	—	`IsIrreducible.closure` `isIrreducible_singleton` `def`
`mem` 📖	mathematical	`IsGenericPoint`	`Set` `Set.instMembership`	—	`specializes_iff_mem` `specializes_rfl`
`mem_closed_set_iff` 📖	mathematical	`IsGenericPoint`	`Set` `Set.instMembership` `Set.instHasSubset`	—	`def` `IsClosed.closure_subset_iff` `Set.singleton_subset_iff`
`mem_open_set_iff` 📖	mathematical	`IsGenericPoint` `IsOpen`	`Set` `Set.instMembership` `Set.Nonempty` `Set.instInter`	—	`mem` `Specializes.mem_open` `specializes`
`specializes` 📖	mathematical	`IsGenericPoint` `Set` `Set.instMembership`	`Specializes`	—	`specializes_iff_mem`
`specializes_iff_mem` 📖	mathematical	`IsGenericPoint`	`Specializes` `Set` `Set.instMembership`	—	`isGenericPoint_iff_specializes`

IsIrreducible

Definitions

Name	Category	Theorems
`genericPoint` 📖	CompOp	4 math math: `genericPoint_closure_eq`, `isGenericPoint_genericPoint_closure`, `isGenericPoint_genericPoint`, `closure_genericPoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_genericPoint` 📖	mathematical	`IsIrreducible`	`closure` `Set` `Set.instSingletonSet` `genericPoint`	—	`isGenericPoint_genericPoint_closure` `IsClosed.closure_eq`
`genericPoint_closure_eq` 📖	mathematical	`IsIrreducible`	`closure` `Set` `Set.instSingletonSet` `genericPoint`	—	`isGenericPoint_genericPoint_closure`
`isGenericPoint_genericPoint` 📖	mathematical	`IsIrreducible`	`IsGenericPoint` `genericPoint`	—	`IsClosed.closure_eq` `isGenericPoint_genericPoint_closure`
`isGenericPoint_genericPoint_closure` 📖	mathematical	`IsIrreducible`	`IsGenericPoint` `genericPoint` `closure`	—	`QuasiSober.sober` `closure` `isClosed_closure`

QuasiSober

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sober` 📖	mathematical	`IsIrreducible`	`IsGenericPoint`	—	—

R1Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiSober` 📖	mathematical	—	`QuasiSober`	—	`IsIrreducible.nonempty` `subset_antisymm` `Set.instAntisymmSubset` `IsClosed.closure_eq` `closure_mono` `Set.singleton_subset_iff` `isPreirreducible_iff_forall_mem_subset_closure_singleton` `IsIrreducible.isPreirreducible`

TopologicalSpace.IsOpenCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiSober` 📖	—	`TopologicalSpace.IsOpenCover` `QuasiSober` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype`	—	—	`quasiSober_iff_forall`
`quasiSober_iff_forall` 📖	mathematical	`TopologicalSpace.IsOpenCover`	`QuasiSober` `TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `instTopologicalSpaceSubtype`	—	`Topology.IsOpenEmbedding.quasiSober` `TopologicalSpace.Opens.isOpenEmbedding'` `quasiSober_iff` `exists_mem` `IsPreirreducible.preimage` `le_antisymm` `IsClosed.closure_subset_iff` `IsClosed.closure_eq` `Continuous.closure_preimage_subset` `continuous_subtype_val` `IsGenericPoint.mem` `IsIrreducible.isGenericPoint_genericPoint_closure` `Set.image_singleton` `closure_image_closure` `IsGenericPoint.def` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure_inter_of_isPreirreducible_of_isOpen` `TopologicalSpace.Opens.isOpen` `closure_mono` `Set.inter_comm` `Set.image_mono` `subset_closure`

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiSober` 📖	mathematical	`Topology.IsClosedEmbedding`	`QuasiSober`	—	`IsIrreducible.image` `Continuous.continuousOn` `continuous` `QuasiSober.sober` `isClosedMap` `IsGenericPoint.mem` `Set.image_injective` `Topology.IsEmbedding.injective` `toIsEmbedding` `IsGenericPoint.def` `closure_image_eq` `Set.image_singleton`

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiSober` 📖	mathematical	`Topology.IsOpenEmbedding`	`QuasiSober`	—	`IsIrreducible.image` `Continuous.continuousOn` `continuous` `QuasiSober.sober` `IsIrreducible.closure` `isClosed_closure` `Topology.IsInducing.isClosed_iff` `isInducing` `IsClosed.closure_eq` `closure_mono` `Set.inter_subset_left` `IsGenericPoint.mem` `Set.image_preimage_eq_inter_range` `IsGenericPoint.mem_open_set_iff` `isOpen_range` `Set.Nonempty.mono` `subset_closure` `Topology.IsEmbedding.closure_eq_preimage_closure_image` `isEmbedding` `Set.image_singleton` `Set.image_injective` `Topology.IsEmbedding.injective` `toIsEmbedding` `Set.ext`

(root)

Definitions

Name	Category	Theorems
`IsGenericPoint` 📖	MathDef	11 math math: `quasiSober_iff`, `isGenericPoint_closure`, `IsIrreducible.isGenericPoint_genericPoint_closure`, `IsIrreducible.isGenericPoint_genericPoint`, `genericPoints.isGenericPoint_ofComponent`, `isGenericPoint_iff_forall_closed`, `isGenericPoint_iff_specializes`, `genericPoints.isGenericPoint`, `genericPoint_spec`, `isGenericPoint_def`, `QuasiSober.sober`
`QuasiSober` 📖	CompData	9 math math: `quasiSober_iff`, `Topology.IsOpenEmbedding.quasiSober`, `PrimeSpectrum.instQuasiSoberElemZeroLocus`, `PrimeSpectrum.quasiSober`, `AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat`, `TopologicalSpace.IsOpenCover.quasiSober_iff_forall`, `Topology.IsClosedEmbedding.quasiSober`, `SpectralSpace.toQuasiSober`, `R1Space.quasiSober`
`genericPoint` 📖	CompOp	8 math math: `genericPoints_eq_singleton`, `AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion`, `AlgebraicGeometry.Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField`, `genericPoint_spec`, `genericPoint_closure`, `genericPoint_specializes`, `AlgebraicGeometry.genericPoint_eq_bot_of_affine`, `AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint`
`genericPoints` 📖	CompOp	9 math math: `genericPoints_eq_singleton`, `genericPoints.component_injective`, `genericPoints.equiv_symm_apply`, `genericPoints.finite`, `genericPoints.closure`, `genericPoints.isGenericPoint_ofComponent`, `genericPoints.component_surjective`, `genericPoints.equiv_apply`, `genericPoints.isGenericPoint`
`irreducibleSetEquivPoints` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`genericPoint_closure` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `genericPoint` `Set.univ`	—	`genericPoint_spec`
`genericPoint_spec` 📖	mathematical	—	`IsGenericPoint` `genericPoint` `Set.univ`	—	`IrreducibleSpace.isIrreducible_univ` `IsClosed.closure_eq` `IsIrreducible.isGenericPoint_genericPoint_closure`
`genericPoint_specializes` 📖	mathematical	—	`Specializes` `genericPoint`	—	`IsGenericPoint.specializes` `IrreducibleSpace.isIrreducible_univ` `IsIrreducible.isGenericPoint_genericPoint_closure` `IsClosed.closure_eq`
`genericPoints_eq_singleton` 📖	mathematical	—	`genericPoints` `Set` `Set.instSingletonSet` `genericPoint`	—	`Set.ext` `genericPoints.eq_1` `irreducibleComponents_eq_singleton` `IsGenericPoint.eq` `genericPoint_spec`
`isGenericPoint_closure` 📖	mathematical	—	`IsGenericPoint` `closure` `Set` `Set.instSingletonSet`	—	`refl` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `eq_isEquiv`
`isGenericPoint_def` 📖	mathematical	—	`IsGenericPoint` `closure` `Set` `Set.instSingletonSet`	—	—
`isGenericPoint_iff_forall_closed` 📖	mathematical	`Set` `Set.instMembership`	`IsGenericPoint` `Set.instHasSubset`	—	`closure_minimal` `Set.singleton_subset_iff` `Set.instReflSubset` `Set.instAntisymmSubset`
`isGenericPoint_iff_specializes` 📖	mathematical	—	`IsGenericPoint` `Specializes` `Set` `Set.instMembership`	—	—
`quasiSober_iff` 📖	mathematical	—	`QuasiSober` `IsGenericPoint`	—	—
`quasiSober_of_open_cover` 📖	—	`IsOpen` `Set` `Set.instMembership` `QuasiSober` `Set.Elem` `instTopologicalSpaceSubtype` `Set.sUnion` `Top.top` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	—	`TopologicalSpace.IsOpenCover.quasiSober` `isOpen_iUnion` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop` `Set.sUnion_eq_iUnion`

genericPoints

Definitions

Name	Category	Theorems
`component` 📖	CompOp	6 math math: `component_injective`, `ofComponent_component`, `component_surjective`, `equiv_apply`, `isGenericPoint`, `component_ofComponent`
`equiv` 📖	CompOp	2 math math: `equiv_symm_apply`, `equiv_apply`
`ofComponent` 📖	CompOp	4 math math: `equiv_symm_apply`, `ofComponent_component`, `isGenericPoint_ofComponent`, `component_ofComponent`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure` 📖	mathematical	—	`closure` `genericPoints` `Set.univ`	—	`Set.eq_univ_iff_forall` `Set.subset_def` `Eq.trans_subset` `irreducibleComponent_mem_irreducibleComponents` `isGenericPoint_ofComponent` `closure_mono` `Set.singleton_subset_iff` `mem_irreducibleComponent`
`component_injective` 📖	mathematical	—	`Set.Elem` `genericPoints` `Set` `irreducibleComponents` `component`	—	`IsGenericPoint.eq` `isGenericPoint`
`component_ofComponent` 📖	mathematical	—	`component` `ofComponent`	—	`isGenericPoint_ofComponent`
`component_surjective` 📖	mathematical	—	`Set.Elem` `genericPoints` `Set` `irreducibleComponents` `component`	—	`component_ofComponent`
`equiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Set.Elem` `genericPoints` `Set` `irreducibleComponents` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `component`	—	—
`equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Set.Elem` `Set` `irreducibleComponents` `genericPoints` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `ofComponent`	—	—
`finite` 📖	mathematical	—	`Set.Finite` `genericPoints`	—	`Finite.of_injective` `component_injective`
`isGenericPoint` 📖	mathematical	—	`IsGenericPoint` `Set` `Set.instMembership` `genericPoints` `irreducibleComponents` `component`	—	—
`isGenericPoint_ofComponent` 📖	mathematical	—	`IsGenericPoint` `Set` `Set.instMembership` `genericPoints` `ofComponent` `irreducibleComponents`	—	`IsIrreducible.isGenericPoint_genericPoint` `isClosed_of_mem_irreducibleComponents`
`ofComponent_component` 📖	mathematical	—	`ofComponent` `component`	—	`component_injective` `component_ofComponent`

---

← Back to Index