mathlib documentation

data.part

Partial values of a type #

This file defines part α, the partial values of a type.

o : part α carries a proposition o.dom, its domain, along with a function get : o.dom → α, its value. The rule is then that every partial value has a value but, to access it, you need to provide a proof of the domain.

part α behaves the same as option α except that o : option α is decidably none or some a for some a : α, while the domain of o : part α doesn't have to be decidable. That means you can translate back and forth between a partial value with a decidable domain and an option, and option α and part α are classically equivalent. In general, part α is bigger than option α.

In current mathlib, part ℕ, aka enat, is used to move decidability of the order to decidability of enat.find (which is the smallest natural satisfying a predicate, or ∞ if there's none).

Main declarations #

option-like declarations:

part.none: The partial value whose domain is false.
part.some a: The partial value whose domain is true and whose value is a.
part.of_option: Converts an option α to a part α by sending none to none and some a to some a.
part.to_option: Converts a part α with a decidable domain to an option α.
part.equiv_option: Classical equivalence between part α and option α.

Monadic structure:

part.bind: o.bind f has value (f (o.get _)).get _ (f o morally) and is defined when o and f (o.get _) are defined.
part.map: Maps the value and keeps the same domain.

Other:

part.restrict: part.restrict p o replaces the domain of o : part α by p : Prop so long as p → o.dom.
part.assert: assert p f appends p to the domains of the values of a partial function.
part.unwrap: Gets the value of a partial value regardless of its domain. Unsound.

Notation #

For a : α, o : part α, a ∈ o means that o is defined and equal to a. Formally, it means o.dom and o.get _ = a.

structure part (α : Type u) :

Type u

dom : Prop
get : self.dom → α

part α is the type of "partial values" of type α. It is similar to option α except the domain condition can be an arbitrary proposition, not necessarily decidable.

def part.to_option {α : Type u_1} (o : part α) [decidable o.dom] :

Convert a part α with a decidable domain to an option

Equations

o.to_option = dite o.dom (λ (h : o.dom), some (o.get h)) (λ (h : ¬o.dom), none)

theorem part.ext' {α : Type u_1} {o p : part α} (H1 : o.dom ↔ p.dom) (H2 : ∀ (h₁ : o.dom) (h₂ : p.dom), o.get h₁ = p.get h₂) :

o = p

part extensionality

@[simp]

theorem part.eta {α : Type u_1} (o : part α) :

{dom := o.dom, get := λ (h : o.dom), o.get h} = o

part eta expansion

@[protected]

def part.mem {α : Type u_1} (a : α) (o : part α) :

Prop

a ∈ o means that o is defined and equal to a

Equations

part.mem a o = ∃ (h : o.dom), o.get h = a

@[protected, instance]

def part.has_mem {α : Type u_1} :

has_mem α (part α)

Equations

part.has_mem = {mem := part.mem α}

theorem part.mem_eq {α : Type u_1} (a : α) (o : part α) :

a ∈ o = ∃ (h : o.dom), o.get h = a

theorem part.dom_iff_mem {α : Type u_1} {o : part α} :

o.dom ↔ ∃ (y : α), y ∈ o

theorem part.get_mem {α : Type u_1} {o : part α} (h : o.dom) :

o.get h ∈ o

@[simp]

theorem part.mem_mk_iff {α : Type u_1} {p : Prop} {o : p → α} {a : α} :

a ∈ {dom := p, get := o} ↔ ∃ (h : p), o h = a

@[ext]

theorem part.ext {α : Type u_1} {o p : part α} (H : ∀ (a : α), a ∈ o ↔ a ∈ p) :

o = p

part extensionality

def part.none {α : Type u_1} :

The none value in part has a false domain and an empty function.

Equations

part.none = {dom := false, get := false.rec α}

@[protected, instance]

def part.inhabited {α : Type u_1} :

inhabited (part α)

Equations

part.inhabited = {default := part.none α}

@[simp]

theorem part.not_mem_none {α : Type u_1} (a : α) :

a ∉ part.none

def part.some {α : Type u_1} (a : α) :

The some a value in part has a true domain and the function returns a.

Equations

part.some a = {dom := true, get := λ (_x : true), a}

theorem part.mem_unique {α : Type u_1} {a b : α} {o : part α} :

a ∈ o → b ∈ o → a = b

theorem part.mem.left_unique {α : Type u_1} :

relator.left_unique has_mem.mem

theorem part.get_eq_of_mem {α : Type u_1} {o : part α} {a : α} (h : a ∈ o) (h' : o.dom) :

o.get h' = a

@[protected]

theorem part.subsingleton {α : Type u_1} (o : part α) :

{a : α | a ∈ o}.subsingleton

@[simp]

theorem part.get_some {α : Type u_1} {a : α} (ha : (part.some a).dom) :

(part.some a).get ha = a

theorem part.mem_some {α : Type u_1} (a : α) :

a ∈ part.some a

@[simp]

theorem part.mem_some_iff {α : Type u_1} {a b : α} :

b ∈ part.some a ↔ b = a

theorem part.eq_some_iff {α : Type u_1} {a : α} {o : part α} :

o = part.some a ↔ a ∈ o

theorem part.eq_none_iff {α : Type u_1} {o : part α} :

o = part.none ↔ ∀ (a : α), a ∉ o

theorem part.eq_none_iff' {α : Type u_1} {o : part α} :

o = part.none ↔ ¬o.dom

@[simp]

theorem part.some_ne_none {α : Type u_1} (x : α) :

part.some x ≠ part.none

@[simp]

theorem part.none_ne_some {α : Type u_1} (x : α) :

part.none ≠ part.some x

theorem part.ne_none_iff {α : Type u_1} {o : part α} :

o ≠ part.none ↔ ∃ (x : α), o = part.some x

theorem part.eq_none_or_eq_some {α : Type u_1} (o : part α) :

o = part.none ∨ ∃ (x : α), o = part.some x

theorem part.some_injective {α : Type u_1} :

function.injective part.some

@[simp]

theorem part.some_inj {α : Type u_1} {a b : α} :

part.some a = part.some b ↔ a = b

@[simp]

theorem part.some_get {α : Type u_1} {a : part α} (ha : a.dom) :

part.some (a.get ha) = a

theorem part.get_eq_iff_eq_some {α : Type u_1} {a : part α} {ha : a.dom} {b : α} :

a.get ha = b ↔ a = part.some b

theorem part.get_eq_get_of_eq {α : Type u_1} (a : part α) (ha : a.dom) {b : part α} (h : a = b) :

a.get ha = b.get _

theorem part.get_eq_iff_mem {α : Type u_1} {o : part α} {a : α} (h : o.dom) :

o.get h = a ↔ a ∈ o

theorem part.eq_get_iff_mem {α : Type u_1} {o : part α} {a : α} (h : o.dom) :

a = o.get h ↔ a ∈ o

@[simp]

theorem part.none_to_option {α : Type u_1} [decidable part.none.dom] :

part.none.to_option = none

@[simp]

theorem part.some_to_option {α : Type u_1} (a : α) [decidable (part.some a).dom] :

(part.some a).to_option = some a

@[protected, instance]

def part.none_decidable {α : Type u_1} :

decidable part.none.dom

Equations

part.none_decidable = decidable.false

@[protected, instance]

def part.some_decidable {α : Type u_1} (a : α) :

decidable (part.some a).dom

Equations

part.some_decidable a = decidable.true

def part.get_or_else {α : Type u_1} (a : part α) [decidable a.dom] (d : α) :

α

Retrieves the value of a : part α if it exists, and return the provided default value otherwise.

Equations

a.get_or_else d = dite a.dom (λ (ha : a.dom), a.get ha) (λ (ha : ¬a.dom), d)

@[simp]

theorem part.get_or_else_none {α : Type u_1} (d : α) [decidable part.none.dom] :

part.none.get_or_else d = d

@[simp]

theorem part.get_or_else_some {α : Type u_1} (a d : α) [decidable (part.some a).dom] :

(part.some a).get_or_else d = a

@[simp]

theorem part.mem_to_option {α : Type u_1} {o : part α} [decidable o.dom] {a : α} :

a ∈ o.to_option ↔ a ∈ o

@[protected]

theorem part.dom.to_option {α : Type u_1} {o : part α} [decidable o.dom] (h : o.dom) :

o.to_option = ↑(o.get h)

theorem part.to_option_eq_none_iff {α : Type u_1} {a : part α} [decidable a.dom] :

a.to_option = none ↔ ¬a.dom

@[simp]

theorem part.elim_to_option {α : Type u_1} {β : Type u_2} (a : part α) [decidable a.dom] (b : β) (f : α → β) :

a.to_option.elim b f = dite a.dom (λ (h : a.dom), f (a.get h)) (λ (h : ¬a.dom), b)

def part.of_option {α : Type u_1} :

option α → part α

Converts an option α into a part α.

Equations

part.of_option (some a) = part.some a
part.of_option none = part.none

@[simp]

theorem part.mem_of_option {α : Type u_1} {a : α} {o : option α} :

a ∈ part.of_option o ↔ a ∈ o

@[simp]

theorem part.of_option_dom {α : Type u_1} (o : option α) :

(part.of_option o).dom ↔ ↥(o.is_some)

theorem part.of_option_eq_get {α : Type u_1} (o : option α) :

part.of_option o = {dom := ↥(o.is_some), get := option.get o}

@[protected, instance]

def part.has_coe {α : Type u_1} :

has_coe (option α) (part α)

Equations

part.has_coe = {coe := part.of_option α}

@[simp]

theorem part.mem_coe {α : Type u_1} {a : α} {o : option α} :

a ∈ ↑o ↔ a ∈ o

@[simp]

theorem part.coe_none {α : Type u_1} :

↑none = part.none

@[simp]

theorem part.coe_some {α : Type u_1} (a : α) :

↑(some a) = part.some a

@[protected]

theorem part.induction_on {α : Type u_1} {P : part α → Prop} (a : part α) (hnone : P part.none) (hsome : ∀ (a : α), P (part.some a)) :

P a

@[protected, instance]

def part.of_option_decidable {α : Type u_1} (o : option α) :

decidable (part.of_option o).dom

Equations

@[simp]

theorem part.to_of_option {α : Type u_1} (o : option α) :

(part.of_option o).to_option = o

@[simp]

theorem part.of_to_option {α : Type u_1} (o : part α) [decidable o.dom] :

part.of_option o.to_option = o

noncomputable def part.equiv_option {α : Type u_1} :

part α ≃ option α

part α is (classically) equivalent to option α.

Equations

part.equiv_option = {to_fun := λ (o : part α), o.to_option, inv_fun := part.of_option α, left_inv := _, right_inv := _}

@[protected, instance]

def part.partial_order {α : Type u_1} :

partial_order (part α)

We give part α the order where everything is greater than none.

Equations

part.partial_order = {le := λ (x y : part α), ∀ (i : α), i ∈ x → i ∈ y, lt := preorder.lt._default (λ (x y : part α), ∀ (i : α), i ∈ x → i ∈ y), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

@[protected, instance]

def part.order_bot {α : Type u_1} :

order_bot (part α)

Equations

part.order_bot = {bot := part.none α, bot_le := _}

theorem part.le_total_of_le_of_le {α : Type u_1} {x y : part α} (z : part α) (hx : x ≤ z) (hy : y ≤ z) :

x ≤ y ∨ y ≤ x

def part.assert {α : Type u_1} (p : Prop) (f : p → part α) :

assert p f is a bind-like operation which appends an additional condition p to the domain and uses f to produce the value.

Equations

part.assert p f = {dom := ∃ (h : p), (f h).dom, get := λ (ha : ∃ (h : p), (f h).dom), (f _).get _}

@[protected]

def part.bind {α : Type u_1} {β : Type u_2} (f : part α) (g : α → part β) :

The bind operation has value g (f.get), and is defined when all the parts are defined.

Equations

f.bind g = part.assert f.dom (λ (b : f.dom), g (f.get b))

@[simp]

theorem part.map_get {α : Type u_1} {β : Type u_2} (f : α → β) (o : part α) (ᾰ : o.dom) :

(part.map f o).get ᾰ = (f ∘ o.get) ᾰ

def part.map {α : Type u_1} {β : Type u_2} (f : α → β) (o : part α) :

The map operation for part just maps the value and maintains the same domain.

Equations

part.map f o = {dom := o.dom, get := f ∘ o.get}

@[simp]

theorem part.map_dom {α : Type u_1} {β : Type u_2} (f : α → β) (o : part α) :

(part.map f o).dom = o.dom

theorem part.mem_map {α : Type u_1} {β : Type u_2} (f : α → β) {o : part α} {a : α} :

a ∈ o → f a ∈ part.map f o

@[simp]

theorem part.mem_map_iff {α : Type u_1} {β : Type u_2} (f : α → β) {o : part α} {b : β} :

b ∈ part.map f o ↔ ∃ (a : α) (H : a ∈ o), f a = b

@[simp]

theorem part.map_none {α : Type u_1} {β : Type u_2} (f : α → β) :

part.map f part.none = part.none

@[simp]

theorem part.map_some {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :

part.map f (part.some a) = part.some (f a)

theorem part.mem_assert {α : Type u_1} {p : Prop} {f : p → part α} {a : α} (h : p) :

a ∈ f h → a ∈ part.assert p f

@[simp]

theorem part.mem_assert_iff {α : Type u_1} {p : Prop} {f : p → part α} {a : α} :

a ∈ part.assert p f ↔ ∃ (h : p), a ∈ f h

theorem part.assert_pos {α : Type u_1} {p : Prop} {f : p → part α} (h : p) :

part.assert p f = f h

theorem part.assert_neg {α : Type u_1} {p : Prop} {f : p → part α} (h : ¬p) :

part.assert p f = part.none

theorem part.mem_bind {α : Type u_1} {β : Type u_2} {f : part α} {g : α → part β} {a : α} {b : β} :

a ∈ f → b ∈ g a → b ∈ f.bind g

@[simp]

theorem part.mem_bind_iff {α : Type u_1} {β : Type u_2} {f : part α} {g : α → part β} {b : β} :

b ∈ f.bind g ↔ ∃ (a : α) (H : a ∈ f), b ∈ g a

@[protected]

theorem part.dom.bind {α : Type u_1} {β : Type u_2} {o : part α} (h : o.dom) (f : α → part β) :

o.bind f = f (o.get h)

theorem part.dom.of_bind {α : Type u_1} {β : Type u_2} {f : α → part β} {a : part α} (h : (a.bind f).dom) :

@[simp]

theorem part.bind_none {α : Type u_1} {β : Type u_2} (f : α → part β) :

part.none.bind f = part.none

@[simp]

theorem part.bind_some {α : Type u_1} {β : Type u_2} (a : α) (f : α → part β) :

(part.some a).bind f = f a

theorem part.bind_of_mem {α : Type u_1} {β : Type u_2} {o : part α} {a : α} (h : a ∈ o) (f : α → part β) :

o.bind f = f a

theorem part.bind_some_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) (x : part α) :

x.bind (part.some ∘ f) = part.map f x

theorem part.bind_to_option {α : Type u_1} {β : Type u_2} (f : α → part β) (o : part α) [decidable o.dom] [Π (a : α), decidable (f a).dom] [decidable (o.bind f).dom] :

(o.bind f).to_option = o.to_option.elim none (λ (a : α), (f a).to_option)

theorem part.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : part α) (g : α → part β) (k : β → part γ) :

(f.bind g).bind k = f.bind (λ (x : α), (g x).bind k)

@[simp]

theorem part.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (x : part α) (g : β → part γ) :

(part.map f x).bind g = x.bind (λ (y : α), g (f y))

@[simp]

theorem part.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → part β) (x : part α) (g : β → γ) :

part.map g (x.bind f) = x.bind (λ (y : α), part.map g (f y))

theorem part.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (o : part α) :

part.map g (part.map f o) = part.map (g ∘ f) o

@[protected, instance]

def part.monad :

Equations

part.monad = monad.mk

@[protected, instance]

def part.is_lawful_monad :

is_lawful_monad part

theorem part.map_id' {α : Type u_1} {f : α → α} (H : ∀ (x : α), f x = x) (o : part α) :

part.map f o = o

@[simp]

theorem part.bind_some_right {α : Type u_1} (x : part α) :

x.bind part.some = x

@[simp]

theorem part.pure_eq_some {α : Type u_1} (a : α) :

pure a = part.some a

@[simp]

theorem part.ret_eq_some {α : Type u_1} (a : α) :

return a = part.some a

@[simp]

theorem part.map_eq_map {α β : Type u_1} (f : α → β) (o : part α) :

f <$> o = part.map f o

@[simp]

theorem part.bind_eq_bind {α β : Type u_1} (f : part α) (g : α → part β) :

f >>= g = f.bind g

theorem part.bind_le {β α : Type u_2} (x : part α) (f : α → part β) (y : part β) :

x >>= f ≤ y ↔ ∀ (a : α), a ∈ x → f a ≤ y

@[protected, instance]

def part.monad_fail :

monad_fail part

Equations

part.monad_fail = {fail := λ (_x : Type u_1) (_x_1 : string), part.none}

def part.restrict {α : Type u_1} (p : Prop) (o : part α) (H : p → o.dom) :

restrict p o h replaces the domain of o with p, and is well defined when p implies o is defined.

Equations

part.restrict p o H = {dom := p, get := λ (h : p), o.get _}

@[simp]

theorem part.mem_restrict {α : Type u_1} (p : Prop) (o : part α) (h : p → o.dom) (a : α) :

a ∈ part.restrict p o h ↔ p ∧ a ∈ o

meta def part.unwrap {α : Type u_1} (o : part α) :

α

unwrap o gets the value at o, ignoring the condition. This function is unsound.

theorem part.assert_defined {α : Type u_1} {p : Prop} {f : p → part α} (h : p) :

(f h).dom → (part.assert p f).dom

theorem part.bind_defined {α : Type u_1} {β : Type u_2} {f : part α} {g : α → part β} (h : f.dom) :

(g (f.get h)).dom → (f.bind g).dom

@[simp]

theorem part.bind_dom {α : Type u_1} {β : Type u_2} {f : part α} {g : α → part β} :

(f.bind g).dom ↔ ∃ (h : f.dom), (g (f.get h)).dom

@[protected, instance]

def part.has_zero {α : Type u_1} [has_zero α] :

has_zero (part α)

Equations

part.has_zero = {zero := pure 0}

@[protected, instance]

def part.has_one {α : Type u_1} [has_one α] :

has_one (part α)

Equations

part.has_one = {one := pure 1}

@[protected, instance]

def part.has_mul {α : Type u_1} [has_mul α] :

has_mul (part α)

Equations

part.has_mul = {mul := λ (a b : part α), has_mul.mul <$> a <*> b}

@[protected, instance]

def part.has_add {α : Type u_1} [has_add α] :

has_add (part α)

Equations

part.has_add = {add := λ (a b : part α), has_add.add <$> a <*> b}

@[protected, instance]

def part.has_neg {α : Type u_1} [has_neg α] :

has_neg (part α)

Equations

part.has_neg = {neg := part.map has_neg.neg}

@[protected, instance]

def part.has_inv {α : Type u_1} [has_inv α] :

has_inv (part α)

Equations

part.has_inv = {inv := part.map has_inv.inv}

@[protected, instance]

def part.has_div {α : Type u_1} [has_div α] :

has_div (part α)

Equations

part.has_div = {div := λ (a b : part α), has_div.div <$> a <*> b}

@[protected, instance]

def part.has_sub {α : Type u_1} [has_sub α] :

has_sub (part α)

Equations

part.has_sub = {sub := λ (a b : part α), has_sub.sub <$> a <*> b}

@[protected, instance]

def part.has_mod {α : Type u_1} [has_mod α] :

has_mod (part α)

Equations

part.has_mod = {mod := λ (a b : part α), has_mod.mod <$> a <*> b}

@[protected, instance]

def part.has_append {α : Type u_1} [has_append α] :

has_append (part α)

Equations

part.has_append = {append := λ (a b : part α), append <$> a <*> b}

@[protected, instance]

def part.has_inter {α : Type u_1} [has_inter α] :

has_inter (part α)

Equations

part.has_inter = {inter := λ (a b : part α), has_inter.inter <$> a <*> b}

@[protected, instance]

def part.has_union {α : Type u_1} [has_union α] :

has_union (part α)

Equations

part.has_union = {union := λ (a b : part α), has_union.union <$> a <*> b}

@[protected, instance]

def part.has_sdiff {α : Type u_1} [has_sdiff α] :

has_sdiff (part α)

Equations

part.has_sdiff = {sdiff := λ (a b : part α), sdiff <$> a <*> b}

theorem part.zero_mem_zero {α : Type u_1} [has_zero α] :

0 ∈ 0

theorem part.one_mem_one {α : Type u_1} [has_one α] :

1 ∈ 1

theorem part.add_mem_add {α : Type u_1} [has_add α] (a b : part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :

ma + mb ∈ a + b

theorem part.mul_mem_mul {α : Type u_1} [has_mul α] (a b : part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :

ma * mb ∈ a * b

theorem part.left_dom_of_add_dom {α : Type u_1} [has_add α] {a b : part α} (hab : (a + b).dom) :

theorem part.left_dom_of_mul_dom {α : Type u_1} [has_mul α] {a b : part α} (hab : (a * b).dom) :

theorem part.right_dom_of_mul_dom {α : Type u_1} [has_mul α] {a b : part α} (hab : (a * b).dom) :

theorem part.right_dom_of_add_dom {α : Type u_1} [has_add α] {a b : part α} (hab : (a + b).dom) :

@[simp]

theorem part.mul_get_eq {α : Type u_1} [has_mul α] (a b : part α) (hab : (a * b).dom) :

(a * b).get hab = (a.get _) * b.get _

@[simp]

theorem part.add_get_eq {α : Type u_1} [has_add α] (a b : part α) (hab : (a + b).dom) :

(a + b).get hab = a.get _ + b.get _

theorem part.some_add_some {α : Type u_1} [has_add α] (a b : α) :

part.some a + part.some b = part.some (a + b)

theorem part.some_mul_some {α : Type u_1} [has_mul α] (a b : α) :

(part.some a) * part.some b = part.some (a * b)

theorem part.neg_mem_neg {α : Type u_1} [has_neg α] (a : part α) (ma : α) (ha : ma ∈ a) :

-ma ∈ -a

theorem part.inv_mem_inv {α : Type u_1} [has_inv α] (a : part α) (ma : α) (ha : ma ∈ a) :

ma⁻¹ ∈ a⁻¹

theorem part.inv_some {α : Type u_1} [has_inv α] (a : α) :

(part.some a)⁻¹ = part.some a⁻¹

theorem part.neg_some {α : Type u_1} [has_neg α] (a : α) :

-part.some a = part.some (-a)

theorem part.div_mem_div {α : Type u_1} [has_div α] (a b : part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :

ma / mb ∈ a / b

theorem part.sub_mem_sub {α : Type u_1} [has_sub α] (a b : part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :

ma - mb ∈ a - b

theorem part.left_dom_of_div_dom {α : Type u_1} [has_div α] {a b : part α} (hab : (a / b).dom) :

theorem part.left_dom_of_sub_dom {α : Type u_1} [has_sub α] {a b : part α} (hab : (a - b).dom) :

theorem part.right_dom_of_sub_dom {α : Type u_1} [has_sub α] {a b : part α} (hab : (a - b).dom) :

theorem part.right_dom_of_div_dom {α : Type u_1} [has_div α] {a b : part α} (hab : (a / b).dom) :

@[simp]

theorem part.sub_get_eq {α : Type u_1} [has_sub α] (a b : part α) (hab : (a - b).dom) :

(a - b).get hab = a.get _ - b.get _

@[simp]

theorem part.div_get_eq {α : Type u_1} [has_div α] (a b : part α) (hab : (a / b).dom) :

(a / b).get hab = a.get _ / b.get _

theorem part.some_div_some {α : Type u_1} [has_div α] (a b : α) :

part.some a / part.some b = part.some (a / b)

theorem part.some_sub_some {α : Type u_1} [has_sub α] (a b : α) :

part.some a - part.some b = part.some (a - b)

theorem part.mod_mem_mod {α : Type u_1} [has_mod α] (a b : part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :

ma % mb ∈ a % b

theorem part.left_dom_of_mod_dom {α : Type u_1} [has_mod α] {a b : part α} (hab : (a % b).dom) :

theorem part.right_dom_of_mod_dom {α : Type u_1} [has_mod α] {a b : part α} (hab : (a % b).dom) :

@[simp]

theorem part.mod_get_eq {α : Type u_1} [has_mod α] (a b : part α) (hab : (a % b).dom) :

(a % b).get hab = a.get _ % b.get _

theorem part.some_mod_some {α : Type u_1} [has_mod α] (a b : α) :

part.some a % part.some b = part.some (a % b)

theorem part.append_mem_append {α : Type u_1} [has_append α] (a b : part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :

ma ++ mb ∈ a ++ b

theorem part.left_dom_of_append_dom {α : Type u_1} [has_append α] {a b : part α} (hab : (a ++ b).dom) :

theorem part.right_dom_of_append_dom {α : Type u_1} [has_append α] {a b : part α} (hab : (a ++ b).dom) :

@[simp]

theorem part.append_get_eq {α : Type u_1} [has_append α] (a b : part α) (hab : (a ++ b).dom) :

(a ++ b).get hab = a.get _ ++ b.get _

theorem part.some_append_some {α : Type u_1} [has_append α] (a b : α) :

part.some a ++ part.some b = part.some (a ++ b)

theorem part.inter_mem_inter {α : Type u_1} [has_inter α] (a b : part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :

ma ∩ mb ∈ a ∩ b

theorem part.left_dom_of_inter_dom {α : Type u_1} [has_inter α] {a b : part α} (hab : (a ∩ b).dom) :

theorem part.right_dom_of_inter_dom {α : Type u_1} [has_inter α] {a b : part α} (hab : (a ∩ b).dom) :

@[simp]

theorem part.inter_get_eq {α : Type u_1} [has_inter α] (a b : part α) (hab : (a ∩ b).dom) :

(a ∩ b).get hab = a.get _ ∩ b.get _

theorem part.some_inter_some {α : Type u_1} [has_inter α] (a b : α) :

part.some a ∩ part.some b = part.some (a ∩ b)

theorem part.union_mem_union {α : Type u_1} [has_union α] (a b : part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :

ma ∪ mb ∈ a ∪ b

theorem part.left_dom_of_union_dom {α : Type u_1} [has_union α] {a b : part α} (hab : (a ∪ b).dom) :

theorem part.right_dom_of_union_dom {α : Type u_1} [has_union α] {a b : part α} (hab : (a ∪ b).dom) :

@[simp]

theorem part.union_get_eq {α : Type u_1} [has_union α] (a b : part α) (hab : (a ∪ b).dom) :

(a ∪ b).get hab = a.get _ ∪ b.get _

theorem part.some_union_some {α : Type u_1} [has_union α] (a b : α) :

part.some a ∪ part.some b = part.some (a ∪ b)

theorem part.sdiff_mem_sdiff {α : Type u_1} [has_sdiff α] (a b : part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :

ma \ mb ∈ a \ b

theorem part.left_dom_of_sdiff_dom {α : Type u_1} [has_sdiff α] {a b : part α} (hab : (a \ b).dom) :

theorem part.right_dom_of_sdiff_dom {α : Type u_1} [has_sdiff α] {a b : part α} (hab : (a \ b).dom) :

@[simp]

theorem part.sdiff_get_eq {α : Type u_1} [has_sdiff α] (a b : part α) (hab : (a \ b).dom) :

(a \ b).get hab = a.get _ \ b.get _

theorem part.some_sdiff_some {α : Type u_1} [has_sdiff α] (a b : α) :

part.some a \ part.some b = part.some (a \ b)