Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-21 23:47 228c00ba

View on Github →

feat(computability/language): le on languages (#5704)

Estimated changes

Modified src/computability/language.lean

modified theorem language.add_self

added theorem language.add_supr

added theorem language.le_add_congr

added theorem language.le_iff

added theorem language.le_mul_congr

added theorem language.mem_add

added theorem language.mem_mul

added theorem language.mem_one

added theorem language.mem_star

added theorem language.mul_self_star_comm

added theorem language.mul_supr

added theorem language.one_add_self_mul_star_eq_star

added theorem language.one_add_star_mul_self_eq_star

added theorem language.star_eq_supr_pow

added theorem language.star_mul_le_left_of_mul_le_left

added theorem language.star_mul_le_right_of_mul_le_right

added theorem language.supr_add

added theorem language.supr_mul

Modified src/order/complete_lattice.lean

added theorem sup_supr

added theorem supr_sup