Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-17 02:10 a2c2bc99

View on Github →

feat(topology/noetherian_space): Noetherian spaces (#14965)

Estimated changes

Modified src/order/compactly_generated.lean

added theorem complete_lattice.{u}

Created src/topology/noetherian_space.lean

added theorem topological_space.noetherian_space.Union

added theorem topological_space.noetherian_space.discrete

added theorem topological_space.noetherian_space.exists_finset_irreducible

added theorem topological_space.noetherian_space.finite

added theorem topological_space.noetherian_space.finite_irreducible_components

added theorem topological_space.noetherian_space.is_compact

added theorem topological_space.noetherian_space.range

added theorem topological_space.noetherian_space_iff_of_homeomorph

added theorem topological_space.noetherian_space_iff_opens

added theorem topological_space.noetherian_space_of_surjective

added theorem topological_space.noetherian_space_set_iff

added theorem topological_space.noetherian_space_tfae

added theorem topological_space.noetherian_univ_iff

Modified src/topology/sets/closeds.lean

modified theorem topological_space.closeds.coe_bot

added theorem topological_space.closeds.coe_finset_inf

added theorem topological_space.closeds.coe_finset_sup

modified theorem topological_space.closeds.coe_inf

modified theorem topological_space.closeds.coe_sup

modified theorem topological_space.closeds.coe_top

added def topological_space.closeds.compl

added theorem topological_space.closeds.compl_bijective

added theorem topological_space.closeds.compl_compl

added def topological_space.opens.compl

added theorem topological_space.opens.compl_bijective

added theorem topological_space.opens.compl_compl

Modified src/topology/sets/opens.lean

modified theorem topological_space.opens.coe_Sup

modified theorem topological_space.opens.coe_bot

added theorem topological_space.opens.coe_finset_inf

added theorem topological_space.opens.coe_finset_sup

modified theorem topological_space.opens.coe_inf

added theorem topological_space.opens.coe_sup

modified theorem topological_space.opens.coe_top

added theorem topological_space.opens.is_compact_element_iff