Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 14:23 ac10136f

View on Github →

feat(algebraic_geometry): The underlying topological space of a Scheme is T0 (#10869)

Estimated changes

Modified src/algebraic_geometry/prime_spectrum/basic.lean

Modified src/algebraic_geometry/properties.lean

Modified src/logic/basic.lean

added theorem not_xor

added theorem xor_iff_not_iff

Modified src/topology/separation.lean

added def indistinguishable

added theorem indistinguishable_iff_closed

added theorem indistinguishable_iff_closure

added theorem subtype_indistinguishable_iff

added theorem t0_space_def

added theorem t0_space_iff_distinguishable

added theorem t0_space_iff_or_not_mem_closure

added theorem t0_space_of_injective_of_continuous