Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-17 00:30 b267edc3

View on Github →

refactor(data/set/countable): define countable in terms of encodable

Estimated changes

Modified analysis/ennreal.lean

Modified analysis/measure_theory/borel_space.lean

Modified analysis/measure_theory/measurable_space.lean

Modified analysis/measure_theory/measure_space.lean

Modified analysis/topology/topological_space.lean

Modified computability/halting.lean

Modified data/equiv/encodable.lean

added theorem encodable.decode2_is_partial_inv

added theorem encodable.mem_decode2'

Modified data/set/countable.lean

added def set.countable.to_encodable

deleted theorem set.countable.to_encodable

modified def set.countable

modified theorem set.countable_encodable'

modified theorem set.countable_encodable

added theorem set.countable_iff_exists_inj_on

added theorem set.countable_iff_exists_injective

modified theorem set.countable_image

added theorem set.countable_range

modified theorem set.countable_set_of_finite_subset

modified theorem set.countable_singleton

Modified data/set/function.lean

added theorem set.inj_on_iff_injective

added theorem set.surj_on_iff_surjective

Modified logic/function.lean

added theorem function.is_partial_inv_left

added theorem function.partial_inv_left