Documentation Verification Report

NoetherianSpace

📁 Source: Mathlib/Topology/NoetherianSpace.lean

Statistics

Metric	Count
Definitions `NoetherianSpace`	1
Theorems `to_noetherianSpace`, `compactSpace`, `discrete`, `exists_finite_set_closeds_irreducible`, `exists_finite_set_isClosed_irreducible`, `exists_finset_irreducible`, `exists_isOpen_nonempty_subset_irreducibleComponent`, `exists_open_ne_empty_le_irreducibleComponent`, `finite`, `finite_irreducibleComponents`, `iUnion`, `isCompact`, `range`, `instNoetherianSpaceCofiniteTopology`, `instWellFoundedLTClosedsOfNoetherianSpace`, `noetherianSpace_TFAE`, `noetherianSpace_iff_isCompact`, `noetherianSpace_iff_of_homeomorph`, `noetherianSpace_iff_opens`, `noetherianSpace_of_surjective`, `noetherianSpace_set_iff`, `noetherian_univ_iff`, `noetherianSpace`	23
Total	24

TopologicalSpace

Definitions

Name	Category	Theorems
`NoetherianSpace` 📖	MathDef	17 math math: `noetherian_univ_iff`, `Topology.IsInducing.noetherianSpace`, `AlgebraicGeometry.noetherianSpace_of_isAffine`, `AlgebraicGeometry.IsNoetherian.noetherianSpace`, `noetherianSpace_iff_of_homeomorph`, `noetherianSpace_of_surjective`, `instNoetherianSpaceCofiniteTopology`, `noetherianSpace_set_iff`, `noetherianSpace_TFAE`, `noetherianSpace_iff_opens`, `Finite.to_noetherianSpace`, `PrimeSpectrum.instNoetherianSpace`, `AlgebraicGeometry.noetherianSpace_of_isAffineOpen`, `NoetherianSpace.set`, `AlgebraicGeometry.instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier`, `noetherianSpace_iff_isCompact`, `NoetherianSpace.range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNoetherianSpaceCofiniteTopology` 📖	mathematical	—	`NoetherianSpace` `CofiniteTopology` `CofiniteTopology.instTopologicalSpace`	—	`CofiniteTopology.nhds_eq` `Ultrafilter.le_cofinite_or_eq_pure` `Filter.nonempty_of_mem` `Ultrafilter.neBot` `le_rfl`
`instWellFoundedLTClosedsOfNoetherianSpace` 📖	mathematical	—	`WellFoundedLT` `Closeds` `Preorder.toLT` `PartialOrder.toPreorder` `Closeds.instPartialOrder`	—	`List.TFAE.out` `noetherianSpace_TFAE`
`noetherianSpace_TFAE` 📖	mathematical	—	`List.TFAE` `NoetherianSpace` `WellFoundedLT` `Closeds` `Preorder.toLT` `PartialOrder.toPreorder` `Closeds.instPartialOrder`	—	`Function.Surjective.wellFounded_iff` `Opens.compl_bijective` `OrderIso.lt_iff_lt` `noetherianSpace_iff_opens` `NoetherianSpace.isCompact` `List.tfae_of_cycle`
`noetherianSpace_iff_isCompact` 📖	mathematical	—	`NoetherianSpace` `IsCompact`	—	`List.TFAE.out` `noetherianSpace_TFAE`
`noetherianSpace_iff_of_homeomorph` 📖	mathematical	—	`NoetherianSpace`	—	`noetherianSpace_of_surjective` `Homeomorph.continuous` `Homeomorph.surjective`
`noetherianSpace_iff_opens` 📖	mathematical	—	`NoetherianSpace` `IsCompact` `SetLike.coe` `Opens` `Opens.instSetLike`	—	`NoetherianSpace.eq_1` `CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact` `CompleteLattice.isSupFiniteCompact_iff_all_elements_compact` `Opens.isCompactElement_iff`
`noetherianSpace_of_surjective` 📖	mathematical	`Continuous`	`NoetherianSpace`	—	`noetherianSpace_iff_isCompact` `Function.Surjective.forall` `Set.image_surjective` `IsCompact.image` `NoetherianSpace.isCompact`
`noetherianSpace_set_iff` 📖	mathematical	—	`NoetherianSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `IsCompact`	—	`Topology.IsEmbedding.isCompact_iff` `Topology.IsEmbedding.subtypeVal`
`noetherian_univ_iff` 📖	mathematical	—	`NoetherianSpace` `Set.Elem` `Set.univ` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`noetherianSpace_iff_of_homeomorph`

TopologicalSpace.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_noetherianSpace` 📖	mathematical	—	`TopologicalSpace.NoetherianSpace`	—	`Finite.wellFounded_of_trans_of_irrefl` `TopologicalSpace.Opens.instFinite` `instIsTransGt` `instIrreflGt`

TopologicalSpace.NoetherianSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace` 📖	mathematical	—	`CompactSpace`	—	`TopologicalSpace.noetherianSpace_iff_opens`
`discrete` 📖	mathematical	—	`DiscreteTopology`	—	`eq_bot_iff` `isClosed_compl_iff` `IsCompact.isClosed` `isCompact`
`exists_finite_set_closeds_irreducible` 📖	mathematical	—	`Set.Finite` `TopologicalSpace.Closeds` `IsIrreducible` `SetLike.coe` `TopologicalSpace.Closeds.instSetLike` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Closeds.instCompleteLattice`	—	`wellFounded_lt` `TopologicalSpace.instWellFoundedLTClosedsOfNoetherianSpace` `eq_or_ne` `instIsEmptyFalse` `sSup_empty` `TopologicalSpace.Closeds.coe_nonempty` `sSup_singleton` `CanLift.prf` `TopologicalSpace.Closeds.instCanLiftSetCoeIsClosed` `inf_lt_left` `Set.Finite.union` `Set.union_subset_iff` `sSup_union` `inf_sup_left` `left_eq_inf`
`exists_finite_set_isClosed_irreducible` 📖	mathematical	—	`Set.Finite` `Set` `IsClosed` `IsIrreducible` `Set.sUnion`	—	`CanLift.prf` `TopologicalSpace.Closeds.instCanLiftSetCoeIsClosed` `exists_finite_set_closeds_irreducible` `Set.Finite.image` `Set.forall_mem_image` `TopologicalSpace.Closeds.isClosed'` `Set.instCanLiftFinsetCoeFinite` `TopologicalSpace.Closeds.coe_finset_sup` `Finset.sup_set_eq_biUnion` `Set.sUnion_image` `Set.iUnion_congr_Prop`
`exists_finset_irreducible` 📖	mathematical	—	`IsIrreducible` `SetLike.coe` `TopologicalSpace.Closeds` `TopologicalSpace.Closeds.instSetLike` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.sup` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Closeds.instCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toBoundedOrder`	—	`Finset.sup_id_eq_sSup` `exists_finite_set_closeds_irreducible`
`exists_isOpen_nonempty_subset_irreducibleComponent` 📖	mathematical	`Set` `Set.instMembership` `irreducibleComponents`	`IsOpen` `Set.Nonempty` `Set.instHasSubset`	—	`finite_irreducibleComponents` `closure_sUnion_irreducibleComponents_diff_singleton` `Set.sUnion_eq_biUnion` `isOpen_compl_iff` `Set.Finite.isClosed_biUnion` `Set.Finite.diff` `isClosed_of_mem_irreducibleComponents` `Mathlib.Tactic.Contrapose.contrapose₁` `closure_empty` `Set.nonempty_iff_empty_ne` `IsIrreducible.nonempty` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `Eq.le`
`exists_open_ne_empty_le_irreducibleComponent` 📖	mathematical	`Set` `Set.instMembership` `irreducibleComponents`	`IsOpen` `Set.Nonempty` `Set.instLE`	—	`exists_isOpen_nonempty_subset_irreducibleComponent`
`finite` 📖	mathematical	—	`Finite`	—	`Finite.of_finite_univ` `IsCompact.finite_of_discrete` `discrete` `isCompact`
`finite_irreducibleComponents` 📖	mathematical	—	`Set.Finite` `Set` `irreducibleComponents`	—	`exists_finite_set_isClosed_irreducible` `isClosed_univ` `Set.Finite.subset` `CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `isIrreducible_iff_sUnion_isClosed` `Set.subset_univ` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset`
`iUnion` 📖	mathematical	`TopologicalSpace.NoetherianSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	`Set.iUnion`	—	`Set.inter_eq_left` `Set.inter_iUnion` `isCompact_iUnion` `Set.inter_subset_right`
`isCompact` 📖	mathematical	—	`IsCompact`	—	`isCompact_iff_finite_subcover` `isOpen_iUnion` `IsCompact.elim_finite_subcover` `TopologicalSpace.noetherianSpace_iff_opens` `Set.Subset.rfl` `HasSubset.Subset.trans` `Set.instIsTransSubset`
`range` 📖	mathematical	`Continuous`	`TopologicalSpace.NoetherianSpace` `Set.Elem` `Set.range` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`TopologicalSpace.noetherianSpace_of_surjective` `Set.mem_range_self` `Set.rangeFactorization_surjective`

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`noetherianSpace` 📖	mathematical	`Topology.IsInducing`	`TopologicalSpace.NoetherianSpace`	—	`TopologicalSpace.noetherianSpace_iff_opens` `isCompact_iff` `TopologicalSpace.NoetherianSpace.isCompact`

---

← Back to Index