Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-15 01:30 3ad35223

View on Github →

feat(data/rat/denumerable): computable denumerability of Q (#1104)

feat(data/rat/denumerable): computable denumerability of Q
blah
fix build
remove unnecessary decidable_eq
add header
delete rat.lean and update imports
fix build
prove exists_not_mem_finset
massively speed up encode
minor change

Estimated changes

Modified src/algebra/archimedean.lean

Modified src/data/equiv/denumerable.lean

added def denumerable.of_encodable_of_infinite

added def nat.subtype.denumerable

added theorem nat.subtype.exists_succ

added theorem nat.subtype.le_succ_of_forall_lt_le

added theorem nat.subtype.lt_succ_iff_le

added theorem nat.subtype.lt_succ_self

added def nat.subtype.of_nat

added theorem nat.subtype.of_nat_surjective

added theorem nat.subtype.of_nat_surjective_aux

added def nat.subtype.succ

added theorem nat.subtype.succ_le_of_lt

Modified src/data/equiv/encodable.lean

added def encodable.decidable_range_encode

added def encodable.equiv_range_encode

Modified src/data/fintype.lean

added theorem infinite.exists_not_mem_finset

added theorem infinite.of_injective

added theorem infinite.of_surjective

Modified src/data/fp/basic.lean

Modified src/data/option/basic.lean

added theorem option.get_some

added theorem option.some_get

Modified src/data/padics/padic_norm.lean

Renamed src/data/rat.lean to src/data/rat/basic.lean

Created src/data/rat/denumerable.lean

Modified src/measure_theory/outer_measure.lean

Modified src/order/bounded_lattice.lean

Modified src/tactic/norm_num.lean