Logic.Vorspiel.Vorspiel

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

source

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

source

@[simp]

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

(Matrix.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) → α

Equations

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

source

@[simp]

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

Matrix.appendr ![] w = w

source

@[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

source

def Matrix.vecToNat {n : ℕ} :

(Fin n → ℕ) → ℕ

Equations

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

source

@[simp]

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

Matrix.vecToNat v = 0

source

@[simp]

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

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

source

def DMatrix.vecEmpty {α : Sort u_1} :

Fin 0 → α

Equations

DMatrix.vecEmpty = Fin.elim0

source

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

α i

Equations

h ::> t = Fin.cons h t

source

def DMatrix.«term_::>_» :

Lean.TrailingParserDescr

Equations

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

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₁ : α 0) (a₂ : α 0) (s₁ : (i : Fin n) → α i.succ) (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 : (i : Fin n) → α i) (w : (i : Fin n) → α i) (h : (i : Fin n) → Decidable (v i = w i)) :

Decidable (v = w)

Equations

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

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 → ℕ)

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

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₂) :

Nat.pair a₁ b₁ ≤ Nat.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 : ι → α) :

Equations

Fintype.sup f = Finset.univ.sup f

source

@[simp]

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

f i ≤ Fintype.sup f

source

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

a ≤ Fintype.sup f

source

@[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

source

@[simp]

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

Fintype.sup f = ⊥

source

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

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

Equations

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

source

def String.vecToStr {n : ℕ} :

(Fin n → String) → String

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

source

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

f = Empty.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} (p : α → Prop) (f : α → β) (g : α → β) :

Prop

Equations

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

source

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

source

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

p 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) → β

Equations

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

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) :

Quotient.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 → α) :

Quotient.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 : α) :

Quotient.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₂ : α) :

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

source

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

Bool

Equations

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

source

def List.upper :

List ℕ → ℕ

Equations

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

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} [DecidableEq α] {β : Type v} [DecidableEq β] {f : α → β} (l : List α) :

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

source

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

l.toFinset ⊆ l'.toFinset

source

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

List α → α

Equations

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

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.getI_map_range {α : Type u} {i : ℕ} {n : ℕ} [Inhabited α] (f : ℕ → α) (h : i < n) :

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

source

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

(List.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} :

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

source

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))

source

theorem List.bind_toList_some {α : Type u} {β : Type v} {f : β → Option α} {g : β → α} {bs : List β} (h : ∀ x ∈ bs, f x = some (g x)) :

(bs.bind fun (i : β) => (f i).toList) = List.map g bs

source

theorem List.mapM'_eq_none_iff {α : Type u_2} {β : Type u_1} {f : α → Option β} {l : List α} :

mapM' f l = none ↔ ∃ a ∈ l, f a = none

source

theorem List.length_mapM' {α : Type u_2} {β : Type u_1} {bs : List β} {f : α → Option β} {as : List α} :

mapM' f as = some bs → bs.length = as.length

source

theorem List.mapM'_mem_inversion {α : Type u_2} {β : Type u_1} {bs : List β} {b : β} {f : α → Option β} {as : List α} (h : mapM' f as = some bs) (hb : b ∈ bs) :

∃ (a : α), f a = some b

source

theorem List.mapM'_eq_mapM'_of_eq {m : Type u_3 → Type u_2} {α : Type u_1} {β : Type u_3} [Monad m] {f : α → m β} {g : α → m β} (l : List α) (hf : ∀ a ∈ l, f a = g a) :

mapM' f l = mapM' g l

source

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)

source

def List.allSome' {α : Type u_1} :

List (Option α) → Option (List α)

Equations

List.allSome' = mapM' id

source

@[simp]

theorem List.mapM_eq_map {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) :

mapM' (fun (x : α) => some (f x)) l = some (List.map f l)

source

theorem List.mapM_map {α : Type u_2} {β : Type u_3} {γ : Type u_1} (as : List α) (f : α → Option β) (g : Option β → Option γ) :

mapM' g (List.map f as) = mapM' (g ∘ f) as

source

@[simp]

theorem List.allSome_map_some {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) :

(List.map (fun (x : α) => some (f x)) l).allSome' = some (List.map f l)

source

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

l₁ ++ l ⊆ l₂ ++ l

source

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

l₁ ⊆ l₂

source

theorem List.nil_iff {α : Type u_1} {l : List α} :

l = [] ↔ ∀ (a : α), a ∉ l

source

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

List α → List α

Equations

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

source

@[simp]

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

List.remove a [] = []

source

@[simp]

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

List.remove q (q :: l) = List.remove q l

source

@[simp]

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

List.remove q [p] = [p]

source

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

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

source

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

b ∈ l

source

@[simp]

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

List.remove a (a :: l) = List.remove a l

source

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

source

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

List.remove a l ⊆ l

source

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₂

source

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

source

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)

source

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)

source

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

v.get 1 = v.tail.head

source

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

Mathlib.Vector.ofFn (a :> v) = a ::ᵥ Mathlib.Vector.ofFn v

source

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

Finset α

Equations

Finset.rangeOfFinite f = ⋯.toFinset

source

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

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

source

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)

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 : Finset α} {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 : α ≃ α') :

Finset.image (⇑e) Finset.univ = Finset.univ

source

@[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

source

theorem Finset.sup_univ_list_eq_sup_map {σ : Type u_1} {α : Type u_2} [SemilatticeSup α] [OrderBot α] (l : List σ) (f : σ → α) :

(Finset.univ.sup fun (i : Fin l.length) => f l[i]) = (List.map f l).sup

source

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

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

source

@[irreducible]

theorem Denumerable.lt_of_mem_list (n : ℕ) (i : ℕ) :

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

source

@[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

source

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

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

source

class Exp (α : Type u_1) :

Type u_1

exp : α → α

Instances

source

@[simp]

theorem Set.subset_triunion₁ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) :

s₁ ⊆ s₁ ∪ s₂ ∪ s₃

source

@[simp]

theorem Set.subset_triunion₂ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) :

s₂ ⊆ s₁ ∪ s₂ ∪ s₃

source

@[simp]

theorem Set.subset_triunion₃ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) :

s₃ ⊆ s₁ ∪ s₂ ∪ s₃

source

@[simp]

theorem Set.subset_tetraunion₁ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) (s₄ : Set F) :

s₁ ⊆ s₁ ∪ s₂ ∪ s₃ ∪ s₄

source

@[simp]

theorem Set.subset_tetraunion₂ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) (s₄ : Set F) :

s₂ ⊆ s₁ ∪ s₂ ∪ s₃ ∪ s₄

source

@[simp]

theorem Set.subset_tetraunion₃ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) (s₄ : Set F) :

s₃ ⊆ s₁ ∪ s₂ ∪ s₃ ∪ s₄

source

@[simp]

theorem Set.subset_tetraunion₄ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) (s₄ : Set F) :

s₄ ⊆ s₁ ∪ s₂ ∪ s₃ ∪ s₄

source

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

Type

Class for α has at least n elements

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

Instances

source

theorem Atleast.mapping {n : ℕ+} {α : Sort u_1} [self : Atleast n α] :

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