Commit 2024-11-25 11:42 8defd9fe

View on Github →

chore(Filter): move defs of Filter.IsBounded etc (#19358)

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Bounded.lean

Modified Mathlib/Order/Filter/Defs.lean

added def Filter.IsBounded

added def Filter.IsBoundedUnder

added def Filter.IsCobounded

added def Filter.IsCoboundedUnder

Modified Mathlib/Order/LiminfLimsup.lean

deleted def Filter.IsBounded

deleted def Filter.IsBoundedUnder

deleted def Filter.IsCobounded

deleted def Filter.IsCoboundedUnder

Modified Mathlib/Topology/Bornology/Basic.lean