Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-09 06:04 42f5ea06

View on Github →

feat(data/semiquot): semiquotient types

Estimated changes

Modified data/fp/basic.lean

deleted def fp.float.default_nan

deleted structure fp.nan_pl

deleted def fp.shift2

added def int.shift2

Modified data/quot.lean

added theorem true_equivalence

added def trunc.bind

added def trunc.map

Modified data/rat.lean

added theorem rat.num_nonneg_iff_zero_le

added theorem rat.num_pos_iff_pos

Created data/semiquot.lean

added def semiquot.bind

added def semiquot.blur'

added def semiquot.blur

added theorem semiquot.blur_eq_blur'

added theorem semiquot.eq_mk_of_mem

added theorem semiquot.eq_pure

added theorem semiquot.exists_mem

added theorem semiquot.ext

added theorem semiquot.ext_s

added def semiquot.get

added theorem semiquot.get_mem

added def semiquot.is_pure

added theorem semiquot.is_pure_of_subsingleton

added theorem semiquot.is_pure_univ

added def semiquot.lift_on

added theorem semiquot.lift_on_of_mem

added def semiquot.map

added theorem semiquot.mem_bind

added theorem semiquot.mem_blur'

added theorem semiquot.mem_map

added theorem semiquot.mem_pure'

added theorem semiquot.mem_pure

added theorem semiquot.mem_pure_self

added theorem semiquot.mem_univ

added def semiquot.mk

added theorem semiquot.ne_empty

added def semiquot.of_trunc

added theorem semiquot.pure_is_pure

added theorem semiquot.pure_le

added def semiquot.to_trunc

added def semiquot.univ

added theorem semiquot.univ_unique

added structure {u}

Modified data/set/lattice.lean

added theorem set.mem_bInter_iff

added theorem set.mem_bUnion_iff

Modified logic/basic.lean

added theorem eq_equivalence