Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-22 20:22 f8464e35

View on Github →

chore(computability/language): golf some proofs (#7301)

Estimated changes

Modified src/computability/language.lean

added theorem language.mem_pow

added theorem language.mem_supr

modified theorem language.mul_def

Modified src/data/list/basic.lean

modified theorem list.join_eq_nil

added theorem list.join_filter_empty_eq_ff

added theorem list.join_filter_ne_nil

Modified src/data/set/lattice.lean

added theorem set.image2_Union_left

added theorem set.image2_Union_right

Modified src/order/complete_lattice.lean

added theorem inf_infi_nat_succ

added theorem sup_supr_nat_succ