Documentation

MathematicalLogic.Part

source
theorem Part.dom_of_mem {α : Type u_1} {a : α} {o : Part α} (h : a ∈ o) :
o.Dom
source
def Part.bindVec {α : Type u_1} {n : ℕ} (v : Vec (Part α) n) :
Part (Vec α n)
Equations
Instances For
    source
    @[simp]
    theorem Part.bindVec_dom {α✝ : Type u_1} {n✝ : ℕ} {v : Vec (Part α✝) n✝} :
    (bindVec v).Dom ↔ ∀ (i : Fin n✝), (v i).Dom
    source
    @[simp]
    theorem Part.mem_bindVec_iff {α✝ : Type u_1} {n✝ : ℕ} {w : Vec (Part α✝) n✝} {v : Vec α✝ n✝} :
    v ∈ bindVec w ↔ ∀ (i : Fin n✝), v i ∈ w i
    source
    @[simp]
    theorem Part.bindVec_get {α✝ : Type u_1} {n✝ : ℕ} {v : Vec (Part α✝) n✝} {h : (bindVec v).Dom} :
    (bindVec v).get h = fun (i : Fin n✝) => (v i).get ⋯
    source
    theorem Part.bindVec_some {α✝ : Type u_1} {n✝ : ℕ} {v : Vec α✝ n✝} :
    (bindVec fun (i : Fin n✝) => some (v i)) = some v
    source
    @[simp]
    theorem Part.bindVec_nil {α : Type u_1} {v : Vec (Part α) 0} :
    bindVec v = some []ᵥ
    source
    theorem Part.bindVec_cons {α : Type u_1} {n : ℕ} {v : Vec (Part α) (n + 1)} :
    bindVec v = do let a ← v.head let w ← bindVec v.tail some (a ∷ᵥ w)
    source
    @[simp]
    theorem Part.bindVec_1 {α : Type u_1} {v : Vec (Part α) 1} :
    bindVec v = do let a ← v 0 some [a]ᵥ
    source
    @[simp]
    theorem Part.bindVec_2 {α : Type u_1} {v : Vec (Part α) 2} :
    bindVec v = do let a ← v 0 let b ← v 1 some [a, b]ᵥ
    source
    @[simp]
    theorem Part.bindVec_3 {α : Type u_1} {v : Vec (Part α) 3} :
    bindVec v = do let a ← v 0 let b ← v 1 let c ← v 2 some [a, b, c]ᵥ
    source
    def Part.natrec {α : Type u_1} (a : Part α) (f : ℕ → α →. α) (n : ℕ) :
    Part α
    Equations
    Instances For
      source
      theorem Part.natrec_zero {α✝ : Type u_1} {a : Part α✝} {f : ℕ → α✝ →. α✝} :
      a.natrec f 0 = a
      source
      theorem Part.natrec_succ {α✝ : Type u_1} {a : Part α✝} {f : ℕ → α✝ →. α✝} {n : ℕ} :
      a.natrec f (n + 1) = do let a ← a.natrec f n f n a
      source
      theorem Part.natrec_dom_le {α✝ : Type u_1} {a : Part α✝} {f : ℕ → α✝ →. α✝} {n k : ℕ} :
      (a.natrec f n).Dom → k ≤ n → (a.natrec f k).Dom
      source
      @[instance 10000]
      instance Part.instPartialOrder_mathematicalLogic {α : Type u} [PartialOrder α] :
      PartialOrder (Part α)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      theorem Part.le_iff {α : Type u} [PartialOrder α] {x y : Part α} :
      x ≤ y ↔ ∀ a ∈ x, ∃ b ∈ y, a ≤ b
      source
      theorem Part.lt_iff {α : Type u} [PartialOrder α] {x y : Part α} :
      x < y ↔ ∃ b ∈ y, ∀ a ∈ x, a < b
      source
      @[simp]
      theorem Part.none_le {α : Type u} [PartialOrder α] {x : Part α} :
      none ≤ x
      source
      @[simp]
      theorem Part.none_lt_some {α : Type u} [PartialOrder α] {a : α} :
      none < some a
      source
      @[simp]
      theorem Part.some_le_some_iff {α : Type u} [PartialOrder α] {a b : α} :
      some a ≤ some b ↔ a ≤ b
      source
      @[simp]
      theorem Part.some_lt_some_iff {α : Type u} [PartialOrder α] {a b : α} :
      some a < some b ↔ a < b
      source
      theorem Part.some_le_iff {α : Type u} [PartialOrder α] {x : Part α} {a : α} :
      some a ≤ x ↔ ∃ b ∈ x, a ≤ b
      source
      theorem Part.some_lt_iff {α : Type u} [PartialOrder α] {x : Part α} {a : α} :
      some a < x ↔ ∃ b ∈ x, a < b
      source
      @[simp]
      theorem Part.zero_lt_some_iff {α : Type u} [PartialOrder α] {a : α} [Zero α] :
      0 < some a ↔ 0 < a
      source
      theorem Part.pos_iff {α : Type u} [PartialOrder α] {x : Part α} [Zero α] :
      0 < x ↔ ∃ a ∈ x, 0 < a
      source
      theorem Part.pos_iff_get {α : Type u} [PartialOrder α] {x : Part α} [Zero α] (h : x.Dom) :
      0 < x ↔ 0 < x.get h
      source
      theorem Part.dom_of_pos {α : Type u} [PartialOrder α] {x : Part α} [Zero α] (h : 0 < x) :
      x.Dom
      source
      @[simp]
      theorem Part.bind_pos_iff {α : Type u} [PartialOrder α] [Zero α] {β : Type u_1} {a : Part β} {f : β → Part α} :
      0 < a.bind f ↔ ∃ x ∈ a, 0 < f x
      source
      theorem Part.zero_or_pos_of_dom {a : Part ℕ} (h : a.Dom) :
      0 < a ∨ 0 ∈ a
      source
      theorem Part.not_pos_iff_of_dom {a : Part ℕ} (h : a.Dom) :
      ¬0 < a ↔ 0 ∈ a
      source
      @[irreducible]
      def Part.find_aux (f : ℕ →. ℕ) (h : ∃ (n : ℕ), 0 < f n ∧ ∀ k < n, (f k).Dom) (n : ℕ) (ih : ∀ k < n, 0 ∈ f k) :
      { n : ℕ // 0 < f n ∧ ∀ k < n, 0 ∈ f k }
      Equations
      Instances For
        source
        def Part.find (f : ℕ →. ℕ) :
        Part ℕ
        Equations
        Instances For
          source
          theorem Part.mem_find_iff {f : ℕ →. ℕ} {n : ℕ} :
          n ∈ find f ↔ 0 < f n ∧ ∀ k < n, 0 ∈ f k
          source
          theorem Part.find_dom {f : ℕ →. ℕ} :
          (find f).Dom ↔ ∃ (n : ℕ), 0 < f n ∧ ∀ k < n, (f k).Dom