Commit 2023-01-02 20:12 0bfc177e

View on Github →

feat: Port data.semiquot (#1275) Port of data.semiquot

Estimated changes

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_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