Commit 2024-03-16 17:36 16cc6aac

View on Github →

feat: review and expand API on behavior of topological bases under some constructions (#10732) The main addition is IsTopologicalBasis.inf (see https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Inf.20of.20a.20pair.20of.20topologies/near/419989448), and I also reordered things to be in the more typical order (deducing the Pi version from the iInf version rather than the converse). Also a few extra golfs and variations.

Estimated changes

Modified Mathlib/Data/Analysis/Topology.lean

Modified Mathlib/Order/Filter/Bases.lean

added theorem Filter.HasBasis.to_image_id'

added theorem Filter.HasBasis.to_image_id

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

Modified Mathlib/Topology/Bases.lean

added theorem IsTopologicalBasis.iInf_induced

added theorem TopologicalSpace.IsTopologicalBasis.inf_induced

added theorem TopologicalSpace.IsTopologicalBasis.of_hasBasis_nhds

deleted theorem isTopologicalBasis_iInf

Modified Mathlib/Topology/Basic.lean

added theorem TopologicalSpace.ext_iff_nhds

Modified Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean

Modified Mathlib/Topology/Maps.lean

added theorem Inducing.basis_nhds

Modified Mathlib/Topology/Order.lean

deleted theorem eq_of_nhds_eq_nhds

Modified Mathlib/Topology/Order/Basic.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean