Commit 2023-12-25 01:16 db487f11

View on Github →

feat(Topology/Order): upgrade continuous_generateFrom to an iff (#9259) Similarly, upgrade tendsto_nhds_generateFrom, IsTopologicalBasis.continuous, Topology.IsLower.continuous_of_Ici, and Topology.IsUpper.continuous_iff_Iic. The old lemmas are now deprecated, and the new ones have _iff in their names. Once we remove the old lemmas, we can drop the _iff suffixes.

Estimated changes

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/Combinatorics/Hindman.lean

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

Modified Mathlib/Topology/Algebra/Order/MonotoneContinuity.lean

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Order.lean

deleted theorem TopologicalSpace.tendsto_nhds_generateFrom

added theorem TopologicalSpace.tendsto_nhds_generateFrom_iff

deleted theorem continuous_generateFrom

added theorem continuous_generateFrom_iff

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

added theorem Topology.IsLower.continuous_iff_Ici

deleted theorem Topology.IsLower.continuous_of_Ici

added theorem Topology.IsUpper.continuous_iff_Iic