Commit 2023-02-08 05:05 63478b6a

View on Github →

feat: port Topology.Filter (#2117)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Filter.lean

added theorem Filter.HasBasis.nhds'

added theorem Filter.continuous_nhds

added theorem Filter.inducing_nhds

added theorem Filter.interₛ_nhds

added theorem Filter.isOpen_Iic_principal

added theorem Filter.isOpen_iff

added theorem Filter.isOpen_setOf_mem

added theorem Filter.isTopologicalBasis_Iic_principal

added theorem Filter.mem_nhds_iff'

added theorem Filter.mem_nhds_iff

added theorem Filter.monotone_nhds

added theorem Filter.nhds_atBot

added theorem Filter.nhds_atTop

added theorem Filter.nhds_bot

added theorem Filter.nhds_eq'

added theorem Filter.nhds_eq

added theorem Filter.nhds_inf

added theorem Filter.nhds_infᵢ

added theorem Filter.nhds_mono

added theorem Filter.nhds_nhds

added theorem Filter.nhds_principal

added theorem Filter.nhds_pure

added theorem Filter.nhds_top

added theorem Filter.specializes_iff_le