Semiquot

📁 Source: Mathlib/Data/Semiquot.lean

Statistics

Metric	Count
Definitions `Semiquot`, `IsPure`, `bind`, `blur`, `blur'`, `get`, `instInhabited`, `instLE`, `instMembership`, `instMonad`, `instOrderTopOfInhabited`, `instSemilatticeSup`, `liftOn`, `map`, `mk`, `ofTrunc`, `partialOrder`, `pure`, `s`, `toTrunc`, `univ`, `val`	22
Theorems `min`, `mono`, `bind_def`, `blur_eq_blur'`, `eq_mk_of_mem`, `eq_pure`, `exists_mem`, `ext`, `ext_s`, `get_mem`, `instLawfulMonad`, `isPure_iff`, `isPure_of_subsingleton`, `isPure_univ`, `liftOn_ofMem`, `map_def`, `mem_bind`, `mem_blur'`, `mem_map`, `mem_pure`, `mem_pure'`, `mem_pure_self`, `mem_univ`, `nonempty`, `pure_inj`, `pure_isPure`, `pure_le`, `univ_unique`	28
Total	50

Semiquot

Definitions

Name	Category	Theorems
`IsPure` 📖	MathDef	4 math math: `isPure_univ`, `isPure_of_subsingleton`, `isPure_iff`, `pure_isPure`
`bind` 📖	CompOp	2 math math: `bind_def`, `mem_bind`
`blur` 📖	CompOp	1 math math: `blur_eq_blur'`
`blur'` 📖	CompOp	2 math math: `mem_blur'`, `blur_eq_blur'`
`get` 📖	CompOp	2 math math: `get_mem`, `eq_pure`
`instInhabited` 📖	CompOp	—
`instLE` 📖	CompOp	2 math math: `IsPure.min`, `pure_le`
`instMembership` 📖	CompOp	11 math math: `mem_map`, `mem_pure_self`, `mem_bind`, `mem_pure'`, `get_mem`, `mem_blur'`, `pure_le`, `mem_pure`, `ext`, `mem_univ`, `exists_mem`
`instMonad` 📖	CompOp	10 math math: `bind_def`, `mem_pure_self`, `instLawfulMonad`, `pure_inj`, `pure_le`, `mem_pure`, `eq_pure`, `isPure_iff`, `map_def`, `pure_isPure`
`instOrderTopOfInhabited` 📖	CompOp	—
`instSemilatticeSup` 📖	CompOp	—
`liftOn` 📖	CompOp	1 math math: `liftOn_ofMem`
`map` 📖	CompOp	2 math math: `mem_map`, `map_def`
`mk` 📖	CompOp	—
`ofTrunc` 📖	CompOp	—
`partialOrder` 📖	CompOp	—
`pure` 📖	CompOp	1 math math: `mem_pure'`
`s` 📖	CompOp	3 math math: `ext_s`, `nonempty`, `eq_mk_of_mem`
`toTrunc` 📖	CompOp	—
`univ` 📖	CompOp	3 math math: `isPure_univ`, `mem_univ`, `univ_unique`
`val` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_def` 📖	mathematical	—	`Semiquot` `instMonad` `bind`	—	—
`blur_eq_blur'` 📖	mathematical	`Set` `Set.instHasSubset` `s`	`blur` `blur'`	—	`Set.union_eq_self_of_subset_right`
`eq_mk_of_mem` 📖	mathematical	`Semiquot` `instMembership`	`s`	—	`ext_s`
`eq_pure` 📖	mathematical	`IsPure`	`Semiquot` `instMonad` `get`	—	`ext` `get_mem`
`exists_mem` 📖	mathematical	—	`Semiquot` `instMembership`	—	`Trunc.exists_rep`
`ext` 📖	mathematical	—	`Semiquot` `instMembership`	—	`ext_s` `Set.ext_iff`
`ext_s` 📖	mathematical	—	`s`	—	`Trunc.instSubsingletonTrunc`
`get_mem` 📖	mathematical	`IsPure`	`Semiquot` `instMembership` `get`	—	`exists_mem` `liftOn_ofMem`
`instLawfulMonad` 📖	mathematical	—	`Semiquot` `instMonad`	—	`ext`
`isPure_iff` 📖	mathematical	—	`IsPure` `Semiquot` `instMonad`	—	`eq_pure` `pure_isPure`
`isPure_of_subsingleton` 📖	mathematical	—	`IsPure`	—	—
`isPure_univ` 📖	mathematical	—	`IsPure` `univ`	—	—
`liftOn_ofMem` 📖	mathematical	`Semiquot` `instMembership`	`liftOn`	—	`eq_mk_of_mem`
`map_def` 📖	mathematical	—	`Semiquot` `instMonad` `map`	—	—
`mem_bind` 📖	mathematical	—	`Semiquot` `instMembership` `bind`	—	`Set.mem_iUnion₂`
`mem_blur'` 📖	mathematical	`Set` `Set.instHasSubset` `s`	`Semiquot` `instMembership` `blur'` `Set.instMembership`	—	—
`mem_map` 📖	mathematical	—	`Semiquot` `instMembership` `map`	—	`Set.mem_image`
`mem_pure` 📖	mathematical	—	`Semiquot` `instMembership` `instMonad`	—	`Set.mem_singleton_iff`
`mem_pure'` 📖	mathematical	—	`Semiquot` `instMembership` `pure`	—	`Set.mem_singleton_iff`
`mem_pure_self` 📖	mathematical	—	`Semiquot` `instMembership` `instMonad`	—	`Set.mem_singleton`
`mem_univ` 📖	mathematical	—	`Semiquot` `instMembership` `univ`	—	`Set.mem_univ`
`nonempty` 📖	mathematical	—	`Set.Nonempty` `s`	—	`exists_mem`
`pure_inj` 📖	mathematical	—	`Semiquot` `instMonad`	—	`ext_s` `Set.singleton_eq_singleton_iff`
`pure_isPure` 📖	mathematical	—	`IsPure` `Semiquot` `instMonad`	—	`mem_pure`
`pure_le` 📖	mathematical	—	`Semiquot` `instLE` `instMonad` `instMembership`	—	`Set.singleton_subset_iff`
`univ_unique` 📖	mathematical	—	`univ`	—	`ext` `refl` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `iff_isEquiv`

Semiquot.IsPure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`min` 📖	mathematical	`Semiquot.IsPure`	`Semiquot` `Semiquot.instLE`	—	`le_antisymm` `Semiquot.eq_pure` `mono` `Semiquot.get_mem` `le_of_eq`
`mono` 📖	—	`Semiquot` `Semiquot.instLE` `Semiquot.IsPure`	—	—	—

(root)

Definitions

Name	Category	Theorems
`Semiquot` 📖	CompData	19 math math: `Semiquot.bind_def`, `Semiquot.mem_map`, `Semiquot.IsPure.min`, `Semiquot.mem_pure_self`, `Semiquot.mem_bind`, `Semiquot.mem_pure'`, `Semiquot.instLawfulMonad`, `Semiquot.pure_inj`, `Semiquot.get_mem`, `Semiquot.mem_blur'`, `Semiquot.pure_le`, `Semiquot.mem_pure`, `Semiquot.eq_pure`, `Semiquot.isPure_iff`, `Semiquot.ext`, `Semiquot.mem_univ`, `Semiquot.map_def`, `Semiquot.exists_mem`, `Semiquot.pure_isPure`

---

← Back to Index