QuasiSeparated

📁 Source: Mathlib/Topology/QuasiSeparated.lean

Statistics

Metric	Count
Definitions IsQuasiSeparated, QuasiSeparatedSpace	2
Theorems inter_of_isOpen, image_of_isEmbedding, of_quasiSeparatedSpace, of_subset, to_quasiSeparatedSpace, inter_isCompact, of_isOpenEmbedding, of_isTopologicalBasis, to_quasiSeparatedSpace, isQuasiSeparated_iff, quasiSeparatedSpace, isQuasiSeparated_iff_quasiSeparatedSpace, isQuasiSeparated_univ, isQuasiSeparated_univ_iff, quasiSeparatedSpace_congr, quasiSeparatedSpace_iff	16
Total	18

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter_of_isOpen 📖	mathematical	IsCompact IsOpen	Set Set.instInter	—	QuasiSeparatedSpace.inter_isCompact

IsQuasiSeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_of_isEmbedding 📖	mathematical	IsQuasiSeparated Topology.IsEmbedding	Set.image	—	Set.preimage_inter Set.image_preimage_eq_inter_range Set.inter_eq_left HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_left Set.image_subset_range IsCompact.image Set.InjOn.mem_image_iff Function.Injective.injOn Topology.IsEmbedding.injective Set.subset_univ Continuous.isOpen_preimage Topology.IsEmbedding.continuous Topology.IsEmbedding.isCompact_iff
of_quasiSeparatedSpace 📖	mathematical	—	IsQuasiSeparated	—	of_subset isQuasiSeparated_univ Set.subset_univ
of_subset 📖	—	IsQuasiSeparated Set Set.instHasSubset	—	—	HasSubset.Subset.trans Set.instIsTransSubset

NoetherianSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_quasiSeparatedSpace 📖	mathematical	—	QuasiSeparatedSpace	—	TopologicalSpace.NoetherianSpace.isCompact

QuasiSeparatedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter_isCompact 📖	mathematical	IsOpen IsCompact	Set Set.instInter	—	—
of_isOpenEmbedding 📖	mathematical	Topology.IsOpenEmbedding	QuasiSeparatedSpace	—	isQuasiSeparated_univ_iff Topology.IsOpenEmbedding.isQuasiSeparated_iff IsQuasiSeparated.of_quasiSeparatedSpace
of_isTopologicalBasis 📖	mathematical	TopologicalSpace.IsTopologicalBasis Set.range Set IsCompact Set.instInter	QuasiSeparatedSpace	—	isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis Set.inter_self Set.iUnion₂_inter_iUnion₂ Set.Finite.isCompact_biUnion

T2Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_quasiSeparatedSpace 📖	mathematical	—	QuasiSeparatedSpace	—	IsCompact.inter

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isQuasiSeparated_iff 📖	mathematical	Topology.IsOpenEmbedding	IsQuasiSeparated Set.image	—	IsQuasiSeparated.image_of_isEmbedding isEmbedding Topology.IsEmbedding.isCompact_iff Set.image_inter Topology.IsEmbedding.injective toIsEmbedding Set.image_mono isOpenMap IsCompact.image continuous
quasiSeparatedSpace 📖	mathematical	Topology.IsOpenEmbedding	QuasiSeparatedSpace	—	isQuasiSeparated_univ_iff isQuasiSeparated_iff IsQuasiSeparated.of_subset isQuasiSeparated_univ Set.subset_univ

(root)

Definitions

Name	Category	Theorems
IsQuasiSeparated 📖	MathDef	6 math math: isQuasiSeparated_univ_iff, IsQuasiSeparated.of_quasiSeparatedSpace, Topology.IsOpenEmbedding.isQuasiSeparated_iff, isQuasiSeparated_univ, AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, isQuasiSeparated_iff_quasiSeparatedSpace
QuasiSeparatedSpace 📖	CompData	25 math math: isQuasiSeparated_univ_iff, AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat, PrimeSpectrum.instQuasiSeparatedSpace, T2Space.to_quasiSeparatedSpace, AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace, SpectralSpace.toQuasiSeparatedSpace, AlgebraicGeometry.IsLocallyNoetherian.quasiSeparatedSpace, AlgebraicGeometry.Scheme.instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated, QuasiSeparatedSpace.of_isTopologicalBasis, AlgebraicGeometry.quasiSeparatedSpace_of_isAffine, AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace, Topology.IsOpenEmbedding.quasiSeparatedSpace, AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens, quasiSeparatedSpace_congr, AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated, NoetherianSpace.to_quasiSeparatedSpace, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated, isQuasiSeparated_iff_quasiSeparatedSpace, AlgebraicGeometry.Scheme.quasiSeparatedSpace_of_isOpenCover, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift, QuasiSeparatedSpace.of_isOpenEmbedding, QuasiSeparatedSpace.of_isOpenCover, AlgebraicGeometry.quasiSeparatedSpace_iff_affine, quasiSeparatedSpace_iff, AlgebraicGeometry.quasiSeparated_over_affine_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isQuasiSeparated_iff_quasiSeparatedSpace 📖	mathematical	IsOpen	IsQuasiSeparated QuasiSeparatedSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	isQuasiSeparated_univ_iff Set.image_univ Subtype.range_coe_subtype Topology.IsOpenEmbedding.isQuasiSeparated_iff IsOpen.isOpenEmbedding_subtypeVal
isQuasiSeparated_univ 📖	mathematical	—	IsQuasiSeparated Set.univ	—	isQuasiSeparated_univ_iff
isQuasiSeparated_univ_iff 📖	mathematical	—	IsQuasiSeparated Set.univ QuasiSeparatedSpace	—	quasiSeparatedSpace_iff
quasiSeparatedSpace_congr 📖	mathematical	—	QuasiSeparatedSpace	—	QuasiSeparatedSpace.of_isOpenEmbedding Homeomorph.isOpenEmbedding
quasiSeparatedSpace_iff 📖	mathematical	—	QuasiSeparatedSpace IsCompact Set Set.instInter	—	—

---

← Back to Index