Documentation

Linglib.Core.Data.Part

Left-biased choice of partial values #

Part.or is the Part analogue of Option.or: p.or q is defined wherever either argument is, with the left taking precedence. Noncomputable, since it decides p.Dom; Flat.or is its computable twin on Option-carried partial values. Also the order facts of the flat domain: definedness is monotone (dom_mono), descent without domain growth is equality (eq_of_le_of_dom), and two partial values are bounded above exactly when they agree wherever both are defined (compat_iff), with p.or q the witnessing bound. [UPSTREAM] candidates for Mathlib/Data/Part.lean.

source
noncomputable def Part.or {α : Type u_1} (p q : Part α) :
Part α

The left-biased choice of two partial values: defined wherever either is, with the left taking precedence.

Equations
  • p.or q = if p.Dom then p else q
Instances For
    source
    @[simp]
    theorem Part.or_dom {α : Type u_1} {p q : Part α} :
    (p.or q).Dom ↔ p.Dom ∨ q.Dom
    source
    theorem Part.mem_or_iff {α : Type u_1} {p q : Part α} {a : α} :
    a ∈ p.or q ↔ a ∈ p ∨ ¬p.Dom ∧ a ∈ q
    source
    @[simp]
    theorem Part.none_or {α : Type u_1} {q : Part α} :
    none.or q = q
    source
    @[simp]
    theorem Part.or_none {α : Type u_1} {p : Part α} :
    p.or none = p
    source
    @[simp]
    theorem Part.some_or {α : Type u_1} {q : Part α} {a : α} :
    (some a).or q = some a
    source
    @[simp]
    theorem Part.bot_or {α : Type u_1} {q : Part α} :
    ⊥.or q = q
    source
    @[simp]
    theorem Part.or_bot {α : Type u_1} {p : Part α} :
    p.or ⊥ = p
    source
    @[simp]
    theorem Part.or_self {α : Type u_1} {p : Part α} :
    p.or p = p
    source
    theorem Part.or_assoc {α : Type u_1} {p q r : Part α} :
    (p.or q).or r = p.or (q.or r)
    source
    theorem Part.le_or_left {α : Type u_1} {p q : Part α} :
    p ≤ p.or q
    source
    theorem Part.or_le {α : Type u_1} {p q r : Part α} (hp : p ≤ r) (hq : q ≤ r) :
    p.or q ≤ r
    source
    theorem Part.dom_mono {α : Type u_1} {p q : Part α} (h : p ≤ q) (hd : p.Dom) :
    q.Dom
    source
    theorem Part.eq_of_le_of_dom {α : Type u_1} {p q : Part α} (h : p ≤ q) (hd : q.Dom → p.Dom) :
    p = q
    source
    theorem Part.le_or_right_of_agree {α : Type u_1} {p q : Part α} (hag : ∀ (a b : α), a ∈ p → b ∈ q → a = b) :
    q ≤ p.or q
    source
    theorem Part.compat_iff {α : Type u_1} {p q : Part α} :
    Compat p q ↔ ∀ (a b : α), a ∈ p → b ∈ q → a = b

    Two partial values are compatible — bounded above in the flat order — exactly when they agree wherever both are defined.

    source
    theorem Part.le_or_right {α : Type u_1} {p q : Part α} (h : Compat p q) :
    q ≤ p.or q