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 →