Commit 2024-08-13 09:26 c074e33e

View on Github →

chore(Topology): remove more bare open Classical (#15671) The only remaining occurrences are in Topology/Algebra.

Estimated changes

Modified Mathlib/Topology/Category/Compactum.lean

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

Modified Mathlib/Topology/Connected/PathConnected.lean

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean

Modified Mathlib/Topology/ContinuousFunction/Compact.lean

Modified Mathlib/Topology/EMetricSpace/Basic.lean

Modified Mathlib/Topology/FiberBundle/Constructions.lean

Modified Mathlib/Topology/Instances/EReal.lean

Modified Mathlib/Topology/Instances/NNReal.lean

modified theorem NNReal.coe_tsum

Modified Mathlib/Topology/Instances/Real.lean

Modified Mathlib/Topology/LocallyConstant/Basic.lean

Modified Mathlib/Topology/MetricSpace/CantorScheme.lean

Modified Mathlib/Topology/MetricSpace/CauSeqFilter.lean

Modified Mathlib/Topology/MetricSpace/Closeds.lean

Modified Mathlib/Topology/MetricSpace/Contracting.lean

Modified Mathlib/Topology/MetricSpace/Dilation.lean

Modified Mathlib/Topology/MetricSpace/Gluing.lean

Modified Mathlib/Topology/MetricSpace/PiNat.lean

Modified Mathlib/Topology/MetricSpace/ThickenedIndicator.lean

Modified Mathlib/Topology/OmegaCompletePartialOrder.lean

Modified Mathlib/Topology/Order/MonotoneConvergence.lean

Modified Mathlib/Topology/UniformSpace/Compact.lean

Modified Mathlib/Topology/UniformSpace/Completion.lean

Modified Mathlib/Topology/UniformSpace/Separation.lean

Modified Mathlib/Topology/VectorBundle/Basic.lean

Modified Mathlib/Topology/VectorBundle/Constructions.lean