Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-01 08:34 2063a528

View on Github →

feat(order/partial_sups): complete lattice lemmas (#8480)

Estimated changes

Modified src/order/partial_sups.lean

modified theorem le_partial_sups

added theorem le_partial_sups_of_le

added theorem monotone.partial_sups_eq

added def partial_sups.gi

modified def partial_sups

deleted theorem partial_sups_eq

added theorem partial_sups_eq_bsupr

added theorem partial_sups_eq_sup'_range

added theorem partial_sups_eq_sup_range

modified theorem partial_sups_le

added theorem partial_sups_mono

modified theorem partial_sups_succ

modified theorem partial_sups_zero

added theorem supr_eq_supr_of_partial_sups_eq_partial_sups

added theorem supr_le_supr_of_partial_sups_le_partial_sups

added theorem supr_partial_sups_eq