Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-09 19:18 d39590fc

View on Github →

refactor(topology/sets/opens): use a structure for opens and open_nhds_of (#18409) Also review API.

Estimated changes

Modified src/algebraic_geometry/AffineScheme.lean

Modified src/algebraic_geometry/Gamma_Spec_adjunction.lean

Modified src/algebraic_geometry/Spec.lean

Modified src/algebraic_geometry/function_field.lean

Modified src/algebraic_geometry/locally_ringed_space.lean

Modified src/algebraic_geometry/locally_ringed_space/has_colimits.lean

Modified src/algebraic_geometry/morphisms/quasi_compact.lean

Modified src/algebraic_geometry/morphisms/quasi_separated.lean

Modified src/algebraic_geometry/morphisms/ring_hom_properties.lean

Modified src/algebraic_geometry/open_immersion.lean

Modified src/algebraic_geometry/presheafed_space.lean

Modified src/algebraic_geometry/presheafed_space/gluing.lean

Modified src/algebraic_geometry/presheafed_space/has_colimits.lean

Modified src/algebraic_geometry/prime_spectrum/basic.lean

Modified src/algebraic_geometry/projective_spectrum/scheme.lean

Modified src/algebraic_geometry/projective_spectrum/topology.lean

Modified src/algebraic_geometry/properties.lean

Modified src/algebraic_geometry/ringed_space.lean

Modified src/algebraic_geometry/stalks.lean

Modified src/algebraic_geometry/structure_sheaf.lean

Modified src/measure_theory/measure/content.lean

added theorem measure_theory.content.inner_content_bot

deleted theorem measure_theory.content.inner_content_empty

Modified src/measure_theory/measure/haar.lean

Modified src/tactic/auto_cases.lean

Modified src/topology/category/Top/opens.lean

Modified src/topology/continuous_function/ideals.lean

Modified src/topology/continuous_function/t0_sierpinski.lean

Modified src/topology/gluing.lean

Modified src/topology/sets/opens.lean

added def homeomorph.opens_congr

added theorem homeomorph.opens_congr_symm

added theorem topological_space.open_nhds_of.basis_nhds

added def topological_space.open_nhds_of.comap

added theorem topological_space.open_nhds_of.to_opens_injective

added structure topological_space.open_nhds_of

deleted def topological_space.open_nhds_of

added theorem topological_space.opens.carrier_eq_coe

added theorem topological_space.opens.coe_inj

modified theorem topological_space.opens.coe_mk

deleted theorem topological_space.opens.comap_val

deleted theorem topological_space.opens.empty_eq

modified theorem topological_space.opens.ext

deleted theorem topological_space.opens.ext_iff

modified def topological_space.opens.gi

deleted theorem topological_space.opens.inter_eq

added theorem topological_space.opens.is_basis.is_compact_open_iff_eq_finite_Union

deleted theorem topological_space.opens.is_compact_open_iff_eq_finite_Union_of_is_basis

deleted theorem topological_space.opens.le_def

deleted theorem topological_space.opens.mem_coe

added theorem topological_space.opens.mk_coe

added def topological_space.opens.simps.coe

deleted theorem topological_space.opens.subset_coe

deleted theorem topological_space.opens.union_eq

deleted theorem topological_space.opens.val_eq_coe

added theorem topological_space.opens.«forall»

added structure topological_space.opens

deleted def topological_space.opens

Modified src/topology/sheaves/presheaf.lean

Modified src/topology/sheaves/punit.lean

Modified src/topology/sheaves/sheaf_condition/sites.lean

modified def Top.sheaf.is_terminal_of_empty

modified def Top.sheaf.is_terminal_of_eq_empty

Modified src/topology/sheaves/stalks.lean