Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-23 08:23 c205fe15

View on Github →

chore(order/conditionally_complete_lattice): golf three proofs (#16064)

Estimated changes

Modified src/analysis/inner_product_space/rayleigh.lean

Modified src/order/conditionally_complete_lattice.lean

deleted theorem cinfi_set

deleted theorem csupr_set