Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-11 12:19 be79f9f3

View on Github →

chore(data/cardinal): put embedding into cardinal namespace

Estimated changes

Modified data/cardinal.lean

added theorem cardinal.embedding.antisymm

added def cardinal.embedding.arrow_congr_left

added def cardinal.embedding.arrow_congr_right

added theorem cardinal.embedding.inj'

added theorem cardinal.embedding.injective_min

added def cardinal.embedding.prod_congr

added theorem cardinal.embedding.refl_apply

added theorem cardinal.embedding.schroeder_bernstein

added def cardinal.embedding.sum_congr

added theorem cardinal.embedding.to_fun_eq_coe

added theorem cardinal.embedding.total

added theorem cardinal.embedding.trans_apply

added structure cardinal.embedding

deleted theorem embedding.antisymm

deleted def embedding.arrow_congr_left

deleted def embedding.arrow_congr_right

deleted theorem embedding.inj'

deleted theorem embedding.injective_min

deleted def embedding.prod_congr

deleted theorem embedding.refl_apply

deleted theorem embedding.schroeder_bernstein

deleted def embedding.sum_congr

deleted theorem embedding.to_fun_eq_coe

deleted theorem embedding.total

deleted theorem embedding.trans_apply

deleted structure embedding

Modified data/ordinal.lean