Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-16 20:12 7bbbee1e

View on Github →

feat(*): various additions to low-level files (#904)

feat(*): various additions to low-level files
fix(data/fin): add missing universe

Estimated changes

Modified src/algebra/order.lean

added def decidable.lt_by_cases

Modified src/data/equiv/basic.lean

added def equiv.subtype_congr_right

added theorem equiv.subtype_congr_right_mk

Modified src/data/fin.lean

added def {u}

Modified src/data/nat/basic.lean

added theorem nat.add_sub_cancel_right

Modified src/data/subtype.lean

added def subtype.coind

added theorem subtype.coind_injective

added theorem subtype.map_injective

added def subtype.restrict

added theorem subtype.restrict_apply

added theorem subtype.restrict_def

added theorem subtype.restrict_injective

modified theorem subtype.val_injective

Modified src/logic/basic.lean

added theorem congr_arg2

Modified src/logic/embedding.lean

Modified src/order/basic.lean

added def bounded

added theorem trans_trichotomous_left

added theorem trans_trichotomous_right

added def unbounded

Modified src/order/order_iso.lean

added theorem injective_of_increasing

Modified src/set_theory/cofinality.lean