Commit 2024-01-12 11:58 9410c2d8

View on Github →

chore(Topology): remove autoImplicit in some files (#9689) ... where this is easy to do.

Estimated changes

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/EMetricSpace/Lipschitz.lean

modified theorem LipschitzOnWith.edist_le_mul_of_le

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

modified theorem Trivialization.tendsto_nhds_iff

Modified Mathlib/Topology/Instances/ENNReal.lean

Modified Mathlib/Topology/MetricSpace/Gluing.lean

Modified Mathlib/Topology/MetricSpace/Kuratowski.lean

modified theorem LipschitzOnWith.extend_lp_infty

Modified Mathlib/Topology/MetricSpace/Lipschitz.lean

Modified Mathlib/Topology/Order/Lattice.lean

Modified Mathlib/Topology/VectorBundle/Basic.lean

modified theorem VectorBundleCore.localTriv_apply