mathlib documentation

data.semiquot

structure semiquot (α : Type u_1) :
Type u_1

A member of semiquot α is classically a nonempty set α, and in the VM is represented by an element of α; the relation between these is that the VM element is required to be a member of the set s. The specific element of s that the VM computes is hidden by a quotient construction, allowing for the representation of nondeterministic functions.

@[instance]
def semiquot.has_mem {α : Type u_1} :
Equations
def semiquot.mk {α : Type u_1} {a : α} {s : set α} (h : a s) :

Construct a semiquot α from h : a ∈ s where s : set α.

Equations
theorem semiquot.ext_s {α : Type u_1} {q₁ q₂ : semiquot α} :
q₁ = q₂ q₁.s = q₂.s
theorem semiquot.ext {α : Type u_1} {q₁ q₂ : semiquot α} :
q₁ = q₂ ∀ (a : α), a q₁ a q₂
theorem semiquot.exists_mem {α : Type u_1} (q : semiquot α) :
∃ (a : α), a q
theorem semiquot.eq_mk_of_mem {α : Type u_1} {q : semiquot α} {a : α} (h : a q) :
theorem semiquot.nonempty {α : Type u_1} (q : semiquot α) :
def semiquot.pure {α : Type u_1} (a : α) :

pure a is a reinterpreted as an unspecified element of {a}.

Equations
@[simp]
theorem semiquot.mem_pure' {α : Type u_1} {a b : α} :
def semiquot.blur' {α : Type u_1} (q : semiquot α) {s : set α} (h : q.s s) :

Replace s in a semiquot with a superset.

Equations
def semiquot.blur {α : Type u_1} (s : set α) (q : semiquot α) :

Replace s in a q : semiquot α with a union s ∪ q.s

Equations
theorem semiquot.blur_eq_blur' {α : Type u_1} (q : semiquot α) (s : set α) (h : q.s s) :
@[simp]
theorem semiquot.mem_blur' {α : Type u_1} (q : semiquot α) {s : set α} (h : q.s s) {a : α} :
a q.blur' h a s
def semiquot.of_trunc {α : Type u_1} (q : trunc α) :

Convert a trunc α to a semiquot α.

Equations
def semiquot.to_trunc {α : Type u_1} (q : semiquot α) :

Convert a semiquot α to a trunc α.

Equations
def semiquot.lift_on {α : Type u_1} {β : Type u_2} (q : semiquot α) (f : α → β) (h : ∀ (a b : α), a qb qf a = f b) :
β

If f is a constant on q.s, then q.lift_on f is the value of f at any point of q.

Equations
theorem semiquot.lift_on_of_mem {α : Type u_1} {β : Type u_2} (q : semiquot α) (f : α → β) (h : ∀ (a b : α), a qb qf a = f b) (a : α) (aq : a q) :
q.lift_on f h = f a
def semiquot.map {α : Type u_1} {β : Type u_2} (f : α → β) (q : semiquot α) :
Equations
@[simp]
theorem semiquot.mem_map {α : Type u_1} {β : Type u_2} (f : α → β) (q : semiquot α) (b : β) :
b semiquot.map f q ∃ (a : α), a q f a = b
def semiquot.bind {α : Type u_1} {β : Type u_2} (q : semiquot α) (f : α → semiquot β) :
Equations
@[simp]
theorem semiquot.mem_bind {α : Type u_1} {β : Type u_2} (q : semiquot α) (f : α → semiquot β) (b : β) :
b q.bind f ∃ (a : α) (H : a q), b f a
@[instance]
Equations
@[simp]
theorem semiquot.map_def {α β : Type u_1} :
@[simp]
theorem semiquot.bind_def {α β : Type u_1} :
@[simp]
theorem semiquot.mem_pure {α : Type u_1} {a b : α} :
a pure b a = b
theorem semiquot.mem_pure_self {α : Type u_1} (a : α) :
a pure a
@[simp]
theorem semiquot.pure_inj {α : Type u_1} {a b : α} :
pure a = pure b a = b
@[instance]
def semiquot.has_le {α : Type u_1} :
Equations
@[instance]
def semiquot.partial_order {α : Type u_1} :
Equations
@[simp]
theorem semiquot.pure_le {α : Type u_1} {a : α} {s : semiquot α} :
pure a s a s
def semiquot.is_pure {α : Type u_1} (q : semiquot α) :
Prop
Equations
def semiquot.get {α : Type u_1} (q : semiquot α) (h : q.is_pure) :
α
Equations
theorem semiquot.get_mem {α : Type u_1} {q : semiquot α} (p : q.is_pure) :
q.get p q
theorem semiquot.eq_pure {α : Type u_1} {q : semiquot α} (p : q.is_pure) :
q = pure (q.get p)
@[simp]
theorem semiquot.pure_is_pure {α : Type u_1} (a : α) :
theorem semiquot.is_pure_iff {α : Type u_1} {s : semiquot α} :
s.is_pure ∃ (a : α), s = pure a
theorem semiquot.is_pure.mono {α : Type u_1} {s t : semiquot α} (st : s t) (h : t.is_pure) :
theorem semiquot.is_pure.min {α : Type u_1} {s t : semiquot α} (h : t.is_pure) :
s t s = t
theorem semiquot.is_pure_of_subsingleton {α : Type u_1} [subsingleton α] (q : semiquot α) :
def semiquot.univ {α : Type u_1} [inhabited α] :

univ : semiquot α represents an unspecified element of univ : set α.

Equations
@[instance]
def semiquot.inhabited {α : Type u_1} [inhabited α] :
Equations
@[simp]
theorem semiquot.mem_univ {α : Type u_1} [inhabited α] (a : α) :
theorem semiquot.univ_unique {α : Type u_1} (I J : inhabited α) :
@[simp]