mathlib3

414df822 - feat(analysis/seminorm): seminorms are a `conditionally_complete_lattice` (#16582)