Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-02 20:12
0bfc177e
View on Github →
feat: Port data.semiquot (
#1275
) Port of data.semiquot
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Data/Semiquot.lean
added
theorem
Semiquot.IsPure.min
added
theorem
Semiquot.IsPure.mono
added
def
Semiquot.IsPure
added
def
Semiquot.bind
added
theorem
Semiquot.bind_def
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
theorem
Semiquot.is_pure_iff
added
theorem
Semiquot.is_pure_of_subsingleton
added
theorem
Semiquot.is_pure_univ
added
def
Semiquot.liftOn
added
theorem
Semiquot.liftOn_ofMem
added
def
Semiquot.map
added
theorem
Semiquot.map_def
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.nonempty
added
def
Semiquot.ofTrunc
added
theorem
Semiquot.pure_inj
added
theorem
Semiquot.pure_is_pure
added
theorem
Semiquot.pure_le
added
def
Semiquot.toTrunc
added
def
Semiquot.univ
added
theorem
Semiquot.univ_unique
added
structure
Semiquot