Commit 2025-04-19 07:34 975550a0

View on Github →

feat(Topology/CompactOpen): basis of the neighborhoods of f : C(X, Y) (#24180)

Estimated changes

Modified Mathlib/Order/CompleteLattice/Basic.lean

Modified Mathlib/Order/Filter/Finite.lean

modified theorem Filter.exists_iInter_of_mem_iInf

added theorem Filter.mem_biInf_principal

modified theorem Filter.mem_iInf_of_finite

Modified Mathlib/Topology/CompactOpen.lean