Commit 2024-02-02 19:14 0311bbc2

View on Github →

feat(Topology): add lift'_nhds_interior etc (#10175)

Estimated changes

Modified Mathlib/Topology/Basic.lean

added theorem Filter.HasBasis.lift'_interior

added theorem Filter.HasBasis.lift'_interior_eq_self

added theorem Filter.HasBasis.nhds_interior

added theorem Filter.lift'_interior_le

added theorem lift'_nhds_interior

Modified Mathlib/Topology/NhdsSet.lean

added theorem Filter.HasBasis.nhdsSet_interior

added theorem lift'_nhdsSet_interior