Commit 2024-10-17 09:17 402539e1

View on Github →

feat(Topology): set of generic points of generic components (#15407)

Estimated changes

Modified Mathlib/AlgebraicGeometry/FunctionField.lean

Modified Mathlib/Topology/Irreducible.lean

added theorem irreducibleComponents_eq_singleton

Modified Mathlib/Topology/Sober.lean

added theorem IsIrreducible.closure_genericPoint

deleted theorem IsIrreducible.genericPoint_spec

added theorem IsIrreducible.isGenericPoint_genericPoint

added theorem IsIrreducible.isGenericPoint_genericPoint_closure

added theorem genericPoints.closure

added def genericPoints.component

added theorem genericPoints.component_injective

added theorem genericPoints.component_ofComponent

added theorem genericPoints.component_surjective

added def genericPoints.equiv

added theorem genericPoints.finite

added theorem genericPoints.isGenericPoint

added theorem genericPoints.isGenericPoint_ofComponent

added def genericPoints.ofComponent

added theorem genericPoints.ofComponent_component

added def genericPoints

added theorem genericPoints_eq_singleton