Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-13 15:02 414df822

View on Github →

feat(analysis/seminorm): seminorms are a conditionally_complete_lattice (#16582)

Estimated changes

Modified src/analysis/seminorm.lean

Modified src/order/conditionally_complete_lattice.lean

added def conditionally_complete_lattice_of_Inf

added def conditionally_complete_lattice_of_Sup

added def conditionally_complete_lattice_of_lattice_of_Inf

added def conditionally_complete_lattice_of_lattice_of_Sup