Commit 2024-08-04 12:42 0b653510

View on Github →

chore(Topology): remove some uses of open Classical (#15481)

Estimated changes

Modified Mathlib/Topology/Algebra/Algebra.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Algebra/Group/Compact.lean

Modified Mathlib/Topology/Algebra/StarSubalgebra.lean

Modified Mathlib/Topology/Algebra/UniformField.lean

Modified Mathlib/Topology/Algebra/UniformGroup.lean

Modified Mathlib/Topology/Algebra/UniformRing.lean

Modified Mathlib/Topology/Clopen.lean

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/Compactness/LocallyCompact.lean

Modified Mathlib/Topology/Compactness/SigmaCompact.lean

modified theorem CompactExhaustion.find_shiftr

modified theorem CompactExhaustion.mem_find

modified theorem CompactExhaustion.mem_iff_find_le

Modified Mathlib/Topology/Connected/Basic.lean

Modified Mathlib/Topology/Connected/Clopen.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/ExtremallyDisconnected.lean

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

Modified Mathlib/Topology/Instances/ENNReal.lean

Modified Mathlib/Topology/Irreducible.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorff.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

Modified Mathlib/Topology/PartitionOfUnity.lean

modified theorem BumpCovering.coe_single

Modified Mathlib/Topology/Separation.lean

Modified Mathlib/Topology/ShrinkingLemma.lean

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

Modified Mathlib/Topology/UnitInterval.lean