Commit 2024-01-25 23:16 79a9e0eb

View on Github →

refactor(Topology/Clopen): order of open and closed (#9957)

Estimated changes

Modified Counterexamples/SorgenfreyLine.lean

Modified Mathlib/FieldTheory/KrullTopology.lean

Modified Mathlib/Topology/AlexandrovDiscrete.lean

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean

Modified Mathlib/Topology/Category/Profinite/CofilteredLimit.lean

Modified Mathlib/Topology/Category/Stonean/Limits.lean

Modified Mathlib/Topology/Clopen.lean

modified theorem isClopen_empty

modified theorem isClopen_univ

Modified Mathlib/Topology/ClopenBox.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Connected/Basic.lean

Modified Mathlib/Topology/Connected/LocallyConnected.lean

Modified Mathlib/Topology/Connected/PathConnected.lean

Modified Mathlib/Topology/Connected/TotallyDisconnected.lean

Modified Mathlib/Topology/DiscreteQuotient.lean

Modified Mathlib/Topology/LocallyConstant/Basic.lean

Modified Mathlib/Topology/SeparatedMap.lean

Modified Mathlib/Topology/Separation.lean

Modified Mathlib/Topology/Sets/Compacts.lean

Modified Mathlib/Topology/StoneCech.lean