Equations
- Nat.«term_:>ₙ_» = Lean.ParserDescr.trailingNode `Nat.term_:>ₙ_ 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :>ₙ ") (Lean.ParserDescr.cat `term 70))
Instances For
Equations
- Matrix.«term_:>_» = Lean.ParserDescr.trailingNode `Matrix.term_:>_ 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :> ") (Lean.ParserDescr.cat `term 70))
Instances For
Equations
- (t <: h) i = Fin.lastCases h t i
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Matrix.«term_<:_» = Lean.ParserDescr.trailingNode `Matrix.term_<:_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <: ") (Lean.ParserDescr.cat `term 71))
Instances For
@[simp]
theorem
Matrix.vecHead_comp
{n : ℕ}
{α : Type u}
{β : Type u_1}
(f : α → β)
(v : Fin (n + 1) → α)
:
Matrix.vecHead (f ∘ v) = f (Matrix.vecHead v)
@[simp]
theorem
Matrix.vecTail_comp
{n : ℕ}
{α : Type u}
{β : Type u_1}
(f : α → β)
(v : Fin (n + 1) → α)
:
Matrix.vecTail (f ∘ v) = f ∘ Matrix.vecTail v
theorem
Matrix.injective_vecCons
{n : ℕ}
{α : Type u}
{f : Fin n → α}
(h : Function.Injective f)
{a : α}
(ha : ∀ (i : Fin n), a ≠ f i)
:
Function.Injective (a :> f)
Equations
- Matrix.toList x_2 = []
- Matrix.toList v = v 0 :: Matrix.toList (v ∘ Fin.succ)
Instances For
@[simp]
theorem
Matrix.toList_succ
{α : Type u_1}
{n : ℕ}
(v : Fin (n + 1) → α)
:
Matrix.toList v = v 0 :: Matrix.toList (v ∘ Fin.succ)
@[simp]
@[simp]
theorem
Matrix.mem_toList_iff
{α : Type u_1}
{n : ℕ}
{v : Fin n → α}
{a : α}
:
a ∈ Matrix.toList v ↔ ∃ (i : Fin n), v i = a
Equations
- Matrix.toOptionVec x_2 = some ![]
- Matrix.toOptionVec v = (Matrix.toOptionVec (v ∘ Fin.succ)).bind fun (vs : Fin n → α) => Option.map (fun (z : α) => z :> vs) (v 0)
Instances For
@[simp]
theorem
Matrix.toOptionVec_some
{α : Type u_1}
{n : ℕ}
(v : Fin n → α)
:
(Matrix.toOptionVec fun (i : Fin n) => some (v i)) = some v
@[simp]
theorem
Matrix.toOptionVec_zero
{α : Type u_1}
(v : Fin 0 → Option α)
:
Matrix.toOptionVec v = some ![]
Equations
- Matrix.getM x_4 = pure finZeroElim
- Matrix.getM f = Seq.seq ((fun (zero : x_3 0) (succ : (i : Fin n) → x_3 i.succ) (i : Fin (n + 1)) => Fin.cases zero succ i) <$> f 0) fun (x : Unit) => Matrix.getM fun (x : Fin n) => f x.succ
Instances For
theorem
Matrix.getM_pure
{m : Type u → Type v}
[Monad m]
[LawfulMonad m]
{n : ℕ}
{β : Fin n → Type u}
(v : (i : Fin n) → β i)
:
(Matrix.getM fun (i : Fin n) => pure (v i)) = pure v
Equations
- Matrix.appendr v w = Matrix.vecAppend ⋯ v w
Instances For
@[simp]
@[simp]
theorem
Matrix.appendr_cons
{α : Type w}
{m : ℕ}
{n : ℕ}
(x : α)
(v : Fin n → α)
(w : Fin m → α)
:
Matrix.appendr (x :> v) w = x :> Matrix.appendr v w
Equations
- Matrix.vecToNat x_2 = 0
- Matrix.vecToNat v = Nat.pair (v 0) (Matrix.vecToNat (v ∘ Fin.succ)) + 1
Instances For
@[simp]
theorem
Matrix.encode_succ
{n : ℕ}
(x : ℕ)
(v : Fin n → ℕ)
:
Matrix.vecToNat (x :> v) = Nat.pair x (Matrix.vecToNat v) + 1
Equations
- DMatrix.vecEmpty = Fin.elim0
Instances For
Equations
- DMatrix.«term_::>_» = Lean.ParserDescr.trailingNode `DMatrix.term_::>_ 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::> ") (Lean.ParserDescr.cat `term 70))
Instances For
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
@[simp]
def
Fintype.sup
{ι : Type u_1}
[Fintype ι]
{α : Type u_2}
[SemilatticeSup α]
[OrderBot α]
(f : ι → α)
:
α
Equations
- Fintype.sup f = Finset.univ.sup f
Instances For
@[simp]
theorem
Fintype.elem_le_sup
{ι : Type u_2}
[Fintype ι]
{α : Type u_1}
[SemilatticeSup α]
[OrderBot α]
(f : ι → α)
(i : ι)
:
f i ≤ Fintype.sup f
theorem
Fintype.le_sup
{ι : Type u_2}
[Fintype ι]
{α : Type u_1}
[SemilatticeSup α]
[OrderBot α]
{a : α}
{f : ι → α}
(i : ι)
(le : a ≤ f i)
:
a ≤ Fintype.sup f
@[simp]
theorem
Fintype.sup_le_iff
{ι : Type u_2}
[Fintype ι]
{α : Type u_1}
[SemilatticeSup α]
[OrderBot α]
{f : ι → α}
{a : α}
:
Fintype.sup f ≤ a ↔ ∀ (i : ι), f i ≤ a
@[simp]
theorem
Fintype.finsup_eq_0_of_empty
{ι : Type u_1}
[Fintype ι]
{α : Type u_2}
[SemilatticeSup α]
[OrderBot α]
[IsEmpty ι]
(f : ι → α)
:
Fintype.sup f = ⊥
def
Fintype.decideEqPi
{ι : Type u_2}
[Fintype ι]
{β : ι → Type u_1}
(a : (i : ι) → β i)
(b : (i : ι) → β i)
:
Equations
- Fintype.decideEqPi a b x = decidable_of_iff (∀ (i : ι), a i = b i) ⋯
Instances For
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
Equations
- Function.funEqOn p f g = ∀ (a : α), p a → f a = g a
Instances For
theorem
Function.funEqOn.of_subset
{α : Type u}
{β : Type v}
{p : α → Prop}
{q : α → Prop}
{f : α → β}
{g : α → β}
(e : Function.funEqOn p f g)
(h : ∀ (a : α), q a → p a)
:
Function.funEqOn q f g
Equations
- One or more equations did not get rendered due to their size.
- Quotient.liftVec f x_4 x_5 = f ![]
Instances For
Instances For
theorem
List.toFinset_map
{α : Type u}
[DecidableEq α]
{β : Type v}
[DecidableEq β]
{f : α → β}
(l : List α)
:
(List.map f l).toFinset = Finset.image f l.toFinset
theorem
List.toFinset_mono
{α : Type u}
[DecidableEq α]
{l : List α}
{l' : List α}
(h : l ⊆ l')
:
l.toFinset ⊆ l'.toFinset
@[simp]
theorem
List.take_map_range
{α : Type u}
{n : ℕ}
{m : ℕ}
(f : ℕ → α)
:
List.take m (List.map f (List.range n)) = List.map f (List.range (min n m))
theorem
List.mapM'_option_map
{α : Type u_3}
{β : Type u_2}
{γ : Type u_1}
{f : α → Option β}
{g : β → γ}
(as : List α)
:
mapM' (fun (a : α) => Option.map g (f a)) as = Option.map (fun (bs : List β) => List.map g bs) (mapM' f as)
Equations
- List.remove a = List.filter fun (x : α) => decide (x ≠ a)
Instances For
@[simp]
theorem
List.eq_remove_cons
{α : Type u_1}
[DecidableEq α]
{q : α}
{l : List α}
:
List.remove q (q :: l) = List.remove q l
@[simp]
theorem
List.remove_singleton_of_ne
{α : Type u_1}
[DecidableEq α]
{p : α}
{q : α}
(h : p ≠ q)
:
List.remove q [p] = [p]
theorem
List.mem_of_mem_remove
{α : Type u_1}
[DecidableEq α]
{a : α}
{b : α}
{l : List α}
(h : b ∈ List.remove a l)
:
b ∈ l
@[simp]
theorem
List.remove_cons_self
{α : Type u_1}
[DecidableEq α]
(l : List α)
(a : α)
:
List.remove a (a :: l) = List.remove a l
theorem
List.remove_cons_of_ne
{α : Type u_1}
[DecidableEq α]
(l : List α)
{a : α}
{b : α}
(ne : a ≠ b)
:
List.remove b (a :: l) = a :: List.remove b l
theorem
List.remove_subset_remove
{α : Type u_1}
[DecidableEq α]
(a : α)
{l₁ : List α}
{l₂ : List α}
(h : l₁ ⊆ l₂)
:
List.remove a l₁ ⊆ List.remove a l₂
theorem
List.remove_cons_subset_cons_remove
{α : Type u_1}
[DecidableEq α]
(a : α)
(b : α)
(l : List α)
:
List.remove b (a :: l) ⊆ a :: List.remove b l
theorem
List.remove_map_substet_map_remove
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[DecidableEq β]
(f : α → β)
(l : List α)
(a : α)
:
List.remove (f a) (List.map f l) ⊆ List.map f (List.remove a l)
theorem
Mathlib.Vector.get_mk_eq_get
{α : Type u_1}
{n : ℕ}
(l : List α)
(h : l.length = n)
(i : Fin n)
:
Mathlib.Vector.get ⟨l, h⟩ i = l.get (Fin.cast ⋯ i)
theorem
Mathlib.Vector.get_one
{α : Type u_2}
{n : ℕ}
(v : Mathlib.Vector α (n + 2))
:
v.get 1 = v.tail.head
theorem
Mathlib.Vector.ofFn_vecCons
{α : Type u_1}
{n : ℕ}
(a : α)
(v : Fin n → α)
:
Mathlib.Vector.ofFn (a :> v) = a ::ᵥ Mathlib.Vector.ofFn v
Equations
- Finset.rangeOfFinite f = ⋯.toFinset
Instances For
theorem
Finset.mem_rangeOfFinite_iff
{α : Type u}
{ι : Sort v}
[Finite ι]
{f : ι → α}
{a : α}
:
a ∈ Finset.rangeOfFinite f ↔ ∃ (i : ι), f i = a
noncomputable def
Finset.imageOfFinset
{α : Type u}
{β : Type v}
[DecidableEq β]
(s : Finset α)
(f : (a : α) → a ∈ s → β)
:
Finset β
Equations
- s.imageOfFinset f = s.biUnion fun (x : α) => Finset.rangeOfFinite (f x)
Instances For
@[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
@[simp]
theorem
Finset.equiv_univ
{α : Type u_1}
{α' : Type u_2}
[Fintype α]
[Fintype α']
[DecidableEq α']
(e : α ≃ α')
:
Finset.image (⇑e) Finset.univ = Finset.univ
@[simp]
theorem
Finset.sup_univ_equiv
{β : Type v}
{α : Type u_1}
{α' : Type u_2}
[DecidableEq α]
[Fintype α]
[Fintype α']
[SemilatticeSup β]
[OrderBot β]
(f : α → β)
(e : α' ≃ α)
:
(Finset.univ.sup fun (i : α') => f (e i)) = Finset.univ.sup f
theorem
Finset.sup_univ_list_eq_sup_map
{σ : Type u_1}
{α : Type u_2}
[SemilatticeSup α]
[OrderBot α]
(l : List σ)
(f : σ → α)
:
@[irreducible]
@[simp]
theorem
Part.mem_vector_mOfFn
{α : Type u_1}
{n : ℕ}
{w : Mathlib.Vector α n}
{v : Fin n →. α}
:
w ∈ Mathlib.Vector.mOfFn v ↔ ∀ (i : Fin n), w.get i ∈ v i
theorem
Atleast.mapping
{n : ℕ+}
{α : Sort u_1}
[self : Atleast n α]
:
∃ (f : Fin ↑n → α), Function.HasLeftInverse f