Vorspiel #

Matrix.getM x_4 = pure finZeroElim
Matrix.getM f = (fun (zero : x_3 0) (succ : (i : Fin n) → x_3 i.succ) (i : Fin (n + 1)) => Fin.cases zero succ i) <$> f 0 <*> Matrix.getM fun (x : Fin n) => f x.succ

Instances For

source

theorem Matrix.getM_pure {m : Type u → Type v} [Monad m] [LawfulMonad m] {n : ℕ} {β : Fin n → Type u} (v : (i : Fin n) → β i) :

(getM fun (i : Fin n) => pure (v i)) = pure v

source

@[simp]

theorem Matrix.getM_some {n : ℕ} {β : Fin n → Type u} (v : (i : Fin n) → β i) :

(getM fun (i : Fin n) => some (v i)) = some v

source

def Matrix.appendr {α : Type w} {n m : ℕ} (v : Fin n → α) (w : Fin m → α) :

Fin (m + n) → α

Imported declaration from the Incompleteness formalization.

Equations

Matrix.appendr v w = Matrix.vecAppend ⋯ v w

Instances For

source

@[simp]

theorem Matrix.appendr_nil {α : Type w} {m : ℕ} (w : Fin m → α) :

appendr ![] w = w

source

@[simp]

theorem Matrix.appendr_cons {α : Type w} {m n : ℕ} (x : α) (v : Fin n → α) (w : Fin m → α) :

appendr (x :> v) w = x :> appendr v w

source

def Matrix.vecToNat {n : ℕ} :

(Fin n → ℕ) → ℕ

Imported declaration from the Incompleteness formalization.

Equations

Matrix.vecToNat x_2 = 0
Matrix.vecToNat v = Nat.pair (v 0) (Matrix.vecToNat (v ∘ Fin.succ)) + 1

Instances For

source

@[simp]

theorem Matrix.vecToNat_empty (v : Fin 0 → ℕ) :

vecToNat v = 0

source

@[simp]

theorem Matrix.encode_succ {n : ℕ} (x : ℕ) (v : Fin n → ℕ) :

vecToNat (x :> v) = Nat.pair x (vecToNat v) + 1

source

def DMatrix.vecEmpty {α : Sort u_1} :

Fin 0 → α

Imported declaration from the Incompleteness formalization.

Equations

DMatrix.vecEmpty = Fin.elim0

Instances For

source

def DMatrix.vecCons {n : ℕ} {α : Fin (n + 1) → Type u_1} (h : α 0) (t : (i : Fin n) → α i.succ) (i : Fin n.succ) :

α i

Imported declaration from the Incompleteness formalization.

Equations

h ::> t = Fin.cons h t

Instances For

source

def DMatrix.«term_::>_» :

Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

DMatrix.«term_::>_» = Lean.ParserDescr.trailingNode `DMatrix.«term_::>_» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::> ") (Lean.ParserDescr.cat `term 70))

Instances For

source

@[simp]

theorem DMatrix.vecCons_zero {n : ℕ} {α : Fin (n + 1) → Type u_1} (h : α 0) (t : (i : Fin n) → α i.succ) :

(h ::> t) 0 = h

source

@[simp]

theorem DMatrix.vecCons_succ {n : ℕ} {α : Fin (n + 1) → Type u_1} (h : α 0) (t : (i : Fin n) → α i.succ) (i : Fin n) :

(h ::> t) i.succ = t i

source

theorem DMatrix.eq_vecCons {n : ℕ} {α : Fin (n + 1) → Type u_1} (s : (i : Fin (n + 1)) → α i) :

s = s 0 ::> fun (i : Fin n) => s i.succ

source

@[simp]

theorem DMatrix.vecCons_ext {n : ℕ} {α : Fin (n + 1) → Type u_1} (a₁ a₂ : α 0) (s₁ s₂ : (i : Fin n) → α i.succ) :

a₁ ::> s₁ = a₂ ::> s₂ ↔ a₁ = a₂ ∧ s₁ = s₂

source

def DMatrix.decVec {n : ℕ} {α : Fin n → Type u_2} (v w : (i : Fin n) → α i) (h : (i : Fin n) → Decidable (v i = w i)) :

Decidable (v = w)

Imported declaration from the Incompleteness formalization.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

pure a = some a

source

@[simp]

theorem Option.toList_eq_iff {α : Type u_1} {o : Option α} {a : α} :

o.toList = [a] ↔ o = some a

source

def Nat.natToVec :

ℕ → (n : ℕ) → Option (Fin n → ℕ)

Imported declaration from the Incompleteness formalization.

Equations

Nat.natToVec 0 0 = some ![]
e.succ.natToVec n.succ = Option.map (fun (x : Fin n → ℕ) => (Nat.unpair e).1 :> x) ((Nat.unpair e).2.natToVec n)
x✝¹.natToVec x✝ = none

Instances For

source

@[simp]

theorem Nat.natToVec_vecToNat {n : ℕ} (v : Fin n → ℕ) :

(Matrix.vecToNat v).natToVec n = some v

source

theorem Nat.lt_of_eq_natToVec {n e : ℕ} {v : Fin n → ℕ} (h : e.natToVec n = some v) (i : Fin n) :

v i < e

source

theorem Nat.one_le_of_bodd {n : ℕ} (h : n.bodd = true) :

1 ≤ n

source

theorem Nat.pair_le_pair_of_le {a₁ a₂ b₁ b₂ : ℕ} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) :

pair a₁ b₁ ≤ pair a₂ b₂

source

theorem Fin.pos_of_coe_ne_zero {n : ℕ} {i : Fin (n + 1)} (h : ↑i ≠ 0) :

0 < i

source

@[simp]

theorem Fin.one_pos'' {n : ℕ} :

0 < 1

source

@[simp]

theorem Fin.two_pos {n : ℕ} :

0 < 2

source

@[simp]

theorem Fin.three_pos {n : ℕ} :

0 < 3

source

@[simp]

theorem Fin.four_pos {n : ℕ} :

0 < 4

source

@[simp]

theorem Fin.five_pos {n : ℕ} :

0 < 5

source

def Fintype.sup {ι : Type u_1} [Fintype ι] {α : Type u_2} [SemilatticeSup α] [OrderBot α] (f : ι → α) :

Imported declaration from the Incompleteness formalization.

Equations

Fintype.sup f = Finset.univ.sup f

Instances For

source

@[simp]

theorem Fintype.elem_le_sup {ι : Type u_2} [Fintype ι] {α : Type u_1} [SemilatticeSup α] [OrderBot α] (f : ι → α) (i : ι) :

f i ≤ sup f

source

theorem Fintype.le_sup {ι : Type u_2} [Fintype ι] {α : Type u_1} [SemilatticeSup α] [OrderBot α] {a : α} {f : ι → α} (i : ι) (le : a ≤ f i) :

a ≤ sup f

source

@[simp]

theorem Fintype.sup_le_iff {ι : Type u_2} [Fintype ι] {α : Type u_1} [SemilatticeSup α] [OrderBot α] {f : ι → α} {a : α} :

sup f ≤ a ↔ ∀ (i : ι), f i ≤ a

source

@[simp]

theorem Fintype.finsup_eq_0_of_empty {ι : Type u_1} [Fintype ι] {α : Type u_2} [SemilatticeSup α] [OrderBot α] [IsEmpty ι] (f : ι → α) :

sup f = ⊥

source

def Fintype.decideEqPi {ι : Type u_2} [Fintype ι] {β : ι → Type u_1} (a b : (i : ι) → β i) :

((i : ι) → Decidable (a i = b i)) → Decidable (a = b)

Imported declaration from the Incompleteness formalization.

Equations

Fintype.decideEqPi a b x✝ = decidable_of_iff (∀ (i : ι), a i = b i) ⋯

Instances For

source

def String.vecToStr {n : ℕ} :

(Fin n → String) → String

Imported declaration from the Incompleteness formalization.

Equations

String.vecToStr x_2 = ""
String.vecToStr s = if n = 0 then s 0 else s 0 ++ ", " ++ String.vecToStr fun (i : Fin n) => s i.succ

Instances For

source

theorem Empty.eq_elim {α : Sort u} (f : Empty → α) :

f = elim

source

theorem IsEmpty.eq_elim {o : Sort u} (h : IsEmpty o) {α : Sort u_1} (f : o → α) :

f = h.elim'

source

def Function.funEqOn {α : Type u} {β : Type v} (φ : α → Prop) (f g : α → β) :

Prop

Imported declaration from the Incompleteness formalization.

Equations

Function.funEqOn φ f g = ∀ (a : α), φ a → f a = g a

Instances For

source

theorem Function.funEqOn.of_subset {α : Type u} {β : Type v} {φ ψ : α → Prop} {f g : α → β} (e : funEqOn φ f g) (h : ∀ (a : α), ψ a → φ a) :

funEqOn ψ f g

source

theorem Quotient.inductionOnVec {α : Type u} [s : Setoid α] {n : ℕ} {φ : (Fin n → Quotient s) → Prop} (v : Fin n → Quotient s) (h : ∀ (v : Fin n → α), φ fun (i : Fin n) => ⟦v i⟧) :

φ v

source

def Quotient.liftVec {α : Type u} [s : Setoid α] {β : Sort v} {n : ℕ} (f : (Fin n → α) → β) :

(∀ (v₁ v₂ : Fin n → α), (∀ (n : Fin n), v₁ n ≈ v₂ n) → f v₁ = f v₂) → (Fin n → Quotient s) → β

Imported declaration from the Incompleteness formalization.

Equations

One or more equations did not get rendered due to their size.
Quotient.liftVec f x_4 x_5 = f ![]

Instances For

source

@[simp]

theorem Quotient.liftVec_zero {α : Type u} [s : Setoid α] {β : Sort v} (f : (Fin 0 → α) → β) (h : ∀ (v₁ v₂ : Fin 0 → α), (∀ (n : Fin 0), v₁ n ≈ v₂ n) → f v₁ = f v₂) (v : Fin 0 → Quotient s) :

liftVec f h v = f ![]

source

theorem Quotient.liftVec_mk {α : Type u} [s : Setoid α] {β : Sort v} {n : ℕ} (f : (Fin n → α) → β) (h : ∀ (v₁ v₂ : Fin n → α), (∀ (n : Fin n), v₁ n ≈ v₂ n) → f v₁ = f v₂) (v : Fin n → α) :

liftVec f h (Quotient.mk s ∘ v) = f v

source

@[simp]

theorem Quotient.liftVec_mk₁ {α : Type u} [s : Setoid α] {β : Sort v} (f : (Fin 1 → α) → β) (h : ∀ (v₁ v₂ : Fin 1 → α), (∀ (n : Fin 1), v₁ n ≈ v₂ n) → f v₁ = f v₂) (a : α) :

liftVec f h ![⟦a⟧] = f ![a]

source

@[simp]

theorem Quotient.liftVec_mk₂ {α : Type u} [s : Setoid α] {β : Sort v} (f : (Fin 2 → α) → β) (h : ∀ (v₁ v₂ : Fin 2 → α), (∀ (n : Fin 2), v₁ n ≈ v₂ n) → f v₁ = f v₂) (a₁ a₂ : α) :

liftVec f h ![⟦a₁⟧, ⟦a₂⟧] = f ![a₁, a₂]

source

theorem List.getI_map_range {α : Type u} {i n : ℕ} [Inhabited α] (f : ℕ → α) (h : i < n) :

(map f (range n)).getI i = f i

source

def List.subsetSet {α : Type u} (l : List α) (s : Set α) [DecidablePred s] :

Bool

Imported declaration from the Incompleteness formalization.

Equations

l.subsetSet s = List.foldr (fun (a : α) (ih : Bool) => decide (s a) && ih) true l

Instances For

source

def List.upper :

List ℕ → ℕ

Imported declaration from the Incompleteness formalization.

Equations

[].upper = 0
(n :: ns).upper = max (n + 1) ns.upper

Instances For

source

@[simp]

theorem List.upper_nil :

[].upper = 0

source

@[simp]

theorem List.upper_cons (n : ℕ) (ns : List ℕ) :

(n :: ns).upper = max (n + 1) ns.upper

source

theorem List.lt_upper (l : List ℕ) {n : ℕ} (h : n ∈ l) :

n < l.upper

source

theorem List.toFinset_map {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (l : List α) :

(map f l).toFinset = Finset.image f l.toFinset

source

theorem List.toFinset_mono {α : Type u} [DecidableEq α] {l l' : List α} (h : l ⊆ l') :

l.toFinset ⊆ l'.toFinset

source

def List.sup {α : Type u} [SemilatticeSup α] [OrderBot α] :

List α → α

Imported declaration from the Incompleteness formalization.

Equations

[].sup = ⊥
(a :: as).sup = a ⊔ as.sup

Instances For

source

@[simp]

theorem List.sup_nil {α : Type u} [SemilatticeSup α] [OrderBot α] :

[].sup = ⊥

source

@[simp]

theorem List.sup_cons {α : Type u} [SemilatticeSup α] [OrderBot α] (a : α) (as : List α) :

(a :: as).sup = a ⊔ as.sup

source

theorem List.le_sup {α : Type u} [SemilatticeSup α] [OrderBot α] {a : α} {l : List α} :

a ∈ l → a ≤ l.sup

source

theorem List.sup_ofFn {α : Type u} [SemilatticeSup α] [OrderBot α] {n : ℕ} (f : Fin n → α) :

(ofFn f).sup = Finset.univ.sup f

source

theorem List.ofFn_get_eq_map_cast {α : Type u} {β : Type v} {n : ℕ} (g : α → β) (as : List α) {h : n = as.length} :

(ofFn fun (i : Fin n) => g (as.get (Fin.cast h i))) = map g as

source

theorem List.append_subset_append {α : Type u_1} {l₁ l₂ l : List α} (h : l₁ ⊆ l₂) :

l₁ ++ l ⊆ l₂ ++ l

source

theorem List.subset_of_eq {α : Type u_1} {l₁ l₂ : List α} (e : l₁ = l₂) :

l₁ ⊆ l₂

source

def List.remove {α : Type u_1} [DecidableEq α] (a : α) :

List α → List α

Imported declaration from the Incompleteness formalization.

Equations

List.remove a = List.filter fun (x : α) => decide (x ≠ a)

Instances For

source

@[simp]

theorem List.remove_nil {α : Type u_1} [DecidableEq α] (a : α) :

remove a [] = []

source

@[simp]

theorem List.eq_remove_cons {α : Type u_1} [DecidableEq α] {ψ : α} {l : List α} :

remove ψ (ψ :: l) = remove ψ l

source

@[simp]

theorem List.remove_singleton_of_ne {α : Type u_1} [DecidableEq α] {φ ψ : α} (h : φ ≠ ψ) :

remove ψ [φ] = [φ]

source

theorem List.mem_remove_iff {α : Type u_1} [DecidableEq α] {a b : α} {l : List α} :

b ∈ remove a l ↔ b ∈ l ∧ b ≠ a

source

theorem List.mem_of_mem_remove {α : Type u_1} [DecidableEq α] {a b : α} {l : List α} (h : b ∈ remove a l) :

b ∈ l

source

theorem List.remove_cons_self {α : Type u_1} [DecidableEq α] (l : List α) (a : α) :

remove a (a :: l) = remove a l

source

theorem List.remove_cons_of_ne {α : Type u_1} [DecidableEq α] (l : List α) {a b : α} (ne : a ≠ b) :

remove b (a :: l) = a :: remove b l

source

theorem List.remove_subset {α : Type u_1} [DecidableEq α] (a : α) (l : List α) :

remove a l ⊆ l

source

theorem List.remove_subset_remove {α : Type u_1} [DecidableEq α] (a : α) {l₁ l₂ : List α} (h : l₁ ⊆ l₂) :

remove a l₁ ⊆ remove a l₂

source

theorem List.remove_cons_subset_cons_remove {α : Type u_1} [DecidableEq α] (a b : α) (l : List α) :

remove b (a :: l) ⊆ a :: remove b l

source

theorem List.remove_map_substet_map_remove {α : Type u_2} {β : Type u_1} [DecidableEq α] [DecidableEq β] (f : α → β) (l : List α) (a : α) :

remove (f a) (map f l) ⊆ map f (remove a l)

source

theorem List.induction_with_singleton {F : Type u_1} {motive : List F → Prop} (hnil : motive []) (hsingle : ∀ (a : F), motive [a]) (hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)) (as : List F) :

motive as

source

theorem List.Vector.get_mk_eq_get {α : Type u_1} {n : ℕ} (l : List α) (h : l.length = n) (i : Fin n) :

get ⟨l, h⟩ i = l.get (Fin.cast ⋯ i)

source

theorem List.Vector.get_one {α : Type u_2} {n : ℕ} (v : Vector α (n + 2)) :

v.get 1 = v.tail.head

source

theorem List.Vector.ofFn_vecCons {α : Type u_1} {n : ℕ} (a : α) (v : Fin n → α) :

ofFn (a :> v) = a ::ᵥ ofFn v

source

noncomputable def Finset.rangeOfFinite {α : Type u} {ι : Sort v} [Finite ι] (f : ι → α) :

Finset α

Imported declaration from the Incompleteness formalization.

Equations

Finset.rangeOfFinite f = ⋯.toFinset

Instances For

source

theorem Finset.mem_rangeOfFinite_iff {α : Type u} {ι : Sort v} [Finite ι] {f : ι → α} {a : α} :

a ∈ rangeOfFinite f ↔ ∃ (i : ι), f i = a

source

noncomputable def Finset.imageOfFinset {α : Type u} {β : Type v} [DecidableEq β] (s : Finset α) (f : (a : α) → a ∈ s → β) :

Finset β

Imported declaration from the Incompleteness formalization.

Equations

s.imageOfFinset f = s.biUnion fun (x : α) => Finset.rangeOfFinite (f x)

Instances For

source

theorem Finset.mem_imageOfFinset_iff {α : Type u} {β : Type v} [DecidableEq β] {s : Finset α} {f : (a : α) → a ∈ s → β} {b : β} :

b ∈ s.imageOfFinset f ↔ ∃ (a : α) (ha : a ∈ s), f a ha = b

source

@[simp]

theorem Finset.mem_imageOfFinset {α : Type u} {β : Type v} [DecidableEq β] {s : Finset α} (f : (a : α) → a ∈ s → β) (a : α) (ha : a ∈ s) :

f a ha ∈ s.imageOfFinset f

source

theorem Finset.erase_union {α : Type u} [DecidableEq α] {a : α} {s t : Finset α} :

(s ∪ t).erase a = s.erase a ∪ t.erase a

source

@[simp]

theorem Finset.equiv_univ {α : Type u_1} {α' : Type u_2} [Fintype α] [Fintype α'] [DecidableEq α'] (e : α ≃ α') :

image (⇑e) univ = univ

source

@[simp]

theorem Finset.sup_univ_equiv {β : Type v} {α : Type u_1} {α' : Type u_2} [Fintype α] [Fintype α'] [SemilatticeSup β] [OrderBot β] (f : α → β) (e : α' ≃ α) :

(univ.sup fun (i : α') => f (e i)) = univ.sup f

source

theorem Finset.sup_univ_cast {α : Type u_1} [SemilatticeSup α] [OrderBot α] {n : ℕ} (f : Fin n → α) (n' : ℕ) {h : n' = n} :

(univ.sup fun (i : Fin n') => f (Fin.cast h i)) = univ.sup f

source

theorem Denumerable.lt_of_mem_list (n i : ℕ) :

i ∈ ofNat (List ℕ) n → i < n

source

@[simp]

theorem Part.mem_vector_mOfFn {α : Type u_1} {n : ℕ} {w : List.Vector α n} {v : Fin n →. α} :

w ∈ List.Vector.mOfFn v ↔ ∀ (i : Fin n), w.get i ∈ v i

source

theorem Set.subset_mem_chain_of_finite {α : Type u_1} (c : Set (Set α)) (hc : c.Nonempty) (hchain : IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) c) {s : Set α} (hfin : s.Finite) :

s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t

source

class Exp (α : Type u_1) :

Type u_1

Imported declaration from the Incompleteness formalization.

exp : α → α
Imported declaration from the Incompleteness formalization.

Instances

source

class Atleast (n : ℕ+) (α : Sort u_1) :

Prop

Class for α has at least n elements

mapping : ∃ (f : Fin ↑n → α), Function.HasLeftInverse f

Instances

Documentation

LeanPool.Incompleteness.Foundation.Vorspiel.Vorspiel

Vorspiel #