Mathlib v3 is deprecated. Go to Mathlib v4

Def conditionally_complete_lattice_of_lattice_of_Inf

Modification history

2022-10-13 15:02
src/order/conditionally_complete_lattice.lean
feat(analysis/seminorm): seminorms are a `conditionally_complete_lattice` (#16582)
Added conditionally_complete_lattice_of_lattice_of_InfView on Github →