Commit 2026-03-18 10:19 0647c6e8

chore(Topology): rename lim -> Filter.lim and limUnder -> Filter.limUnder, and make a lemma protected (#36522) Add the namespace Filter to lim and limUnder, since the docstring for lim suggests that they were never intended to be placed in the namespace. Also make MeasureTheory.StronglyMeasurable.limUnder protected, to allow its proof to refer to Filter.limUnder as limUnder. See discussion here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Rename.20lim.20to.20Filter.2Elim.3F/with/578862980