Commit 2023-02-12 08:52 9e241a03

View on Github →

feat: port Topology.NoetherianSpace (#2219)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Image.lean

added theorem Set.forall_subset_range_iff

added theorem Subtype.forall_set_subtype

Created Mathlib/Topology/NoetherianSpace.lean

added theorem TopologicalSpace.NoetherianSpace.discrete

added theorem TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible

added theorem TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible

added theorem TopologicalSpace.NoetherianSpace.exists_finset_irreducible

added theorem TopologicalSpace.NoetherianSpace.finite

added theorem TopologicalSpace.NoetherianSpace.finite_irreducibleComponents

added theorem TopologicalSpace.NoetherianSpace.range

added theorem TopologicalSpace.NoetherianSpace.unionᵢ

added theorem TopologicalSpace.NoetherianSpace.wellFounded_closeds

added theorem TopologicalSpace.noetherianSpace_TFAE

added theorem TopologicalSpace.noetherianSpace_iff_isCompact

added theorem TopologicalSpace.noetherianSpace_iff_of_homeomorph

added theorem TopologicalSpace.noetherianSpace_iff_opens

added theorem TopologicalSpace.noetherianSpace_of_surjective

added theorem TopologicalSpace.noetherianSpace_set_iff

added theorem TopologicalSpace.noetherian_univ_iff

Modified Mathlib/Topology/Sets/Closeds.lean