accessible lemmas #4
Description
The following lemmas have proofs in LaTeX and statements in Lean. The names here are the names of the Lean declarations.
Point set topology
- WLocalization.stratum_eq_basicOpen_inter_zeroLocus
- compactSpace_connectedComponent
- t2Space_connectedComponent
- WLocalization.stratum_anti
- Prespectral.of_profinite
- Spectral.of_profinite
- Homeomorph.spectralSpace
- IsWLocalMap.comp
- Topology.IsEmbedding.wLocalSpace_of_stableUnderSpecialization_range
- StableUnderSpecialization.generalizationHull_of_wLocalSpace
- Topology.IsClosedEmbedding.wLocalSpace
Commutative algebra
- Ideal.isMaximal_of_isAlgebraic
- range_algebraMap_generalization (nontrivial)