mathlib documentation

data.semiquot

structure semiquot  :
Type u_1Type 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 α} :
a ssemiquot α

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} :
α → semiquot α

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 α} :
q.s ssemiquot α

Replace s in a semiquot with a superset.

Equations
def semiquot.blur {α : Type u_1} :
set αsemiquot α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} :
trunc αsemiquot α

Convert a trunc α to a semiquot α.

Equations
def semiquot.to_trunc {α : Type u_1} :
semiquot αtrunc α

Convert a semiquot α to a trunc α.

Equations
def semiquot.lift_on {α : Type u_1} {β : Type u_2} (q : semiquot α) (f : α → β) :
(∀ (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 : α) :
a qq.lift_on f h = f a

def semiquot.map {α : Type u_1} {β : Type u_2} :
(α → β)semiquot α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} :
semiquot α(α → semiquot β)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} :
semiquot α → Prop

Equations
def semiquot.get {α : Type u_1} (q : semiquot α) :
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 α} :
s tt.is_pure → s.is_pure

theorem semiquot.is_pure.min {α : Type u_1} {s t : semiquot α} :
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]