Supporting results for pointwise provable equality.

@[reducible]

def PointwiseComposition.Finset.toSet {α : Type u_1} (s : Finset α) : Set α

Compatibility shim: mathlib v4.31 removed the named Finset.toSet that used to back the Finset → Set coercion (the coercion is now an inline lambda). Re-introduce the name as a reducible alias for the coercion so existing .toSet call-sites keep elaborating and the Finset.coe_* simp lemmas continue to fire through it.

Equations

• PointwiseComposition.Finset.toSet s = ↑s

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

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

The subset Set construction in List.

Equations

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

def PointwiseComposition.List.upper : List ℕ → ℕ

The upper construction in List.

Equations

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

@[simp]

theorem PointwiseComposition.List.upper_nil : upper [] = 0

@[simp]

theorem PointwiseComposition.List.upper_cons (n : ℕ) (ns : List ℕ) : upper (n :: ns) = max (n + 1) (upper ns)

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

theorem PointwiseComposition.List.toFinset_map {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (l : List α) : (List.map f l).toFinset = Finset.image f l.toFinset

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

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

The sup construction in List.

Equations

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

@[simp]

theorem PointwiseComposition.List.sup_nil {α : Type u} [SemilatticeSup α] [OrderBot α] : sup [] = ⊥

@[simp]

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

theorem PointwiseComposition.List.le_sup {α : Type u} [SemilatticeSup α] [OrderBot α] {a : α} {l : List α} : a ∈ l → a ≤ sup l

theorem PointwiseComposition.List.sup_ofFn {α : Type u} [SemilatticeSup α] [OrderBot α] {n : ℕ} (f : Fin n → α) : sup (List.ofFn f) = Finset.univ.sup f

theorem PointwiseComposition.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

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

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

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

The remove construction in List.

Equations

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

@[simp]

theorem PointwiseComposition.List.remove_nil {α : Type u_1} [DecidableEq α] (a : α) : (fun (x : α) => remove x []) a = []

@[simp]

theorem PointwiseComposition.List.eq_remove_cons {α : Type u_1} [DecidableEq α] {ψ : α} {l : List α} : (fun (x : α) => remove x (ψ :: l)) ψ = (fun (x : α) => remove x l) ψ

@[simp]

theorem PointwiseComposition.List.remove_singleton_of_ne {α : Type u_1} [DecidableEq α] {φ ψ : α} (h : φ ≠ ψ) : (fun (x : α) => remove x [φ]) ψ = [φ]

theorem PointwiseComposition.List.mem_remove_iff {α : Type u_1} [DecidableEq α] {a b : α} {l : List α} : b ∈ (fun (x : α) => remove x l) a ↔ b ∈ l ∧ b ≠ a

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

theorem PointwiseComposition.List.remove_cons_self {α : Type u_1} [DecidableEq α] (l : List α) (a : α) : (fun (x : α) => remove x (a :: l)) a = (fun (x : α) => remove x l) a

theorem PointwiseComposition.List.remove_cons_of_ne {α : Type u_1} [DecidableEq α] (l : List α) {a b : α} (ne : a ≠ b) : (fun (x : α) => remove x (a :: l)) b = a :: (fun (x : α) => remove x l) b

@[simp]

theorem PointwiseComposition.List.remove_subset {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : (fun (x : α) => remove x l) a ⊆ l

@[simp]

theorem PointwiseComposition.List.subset_cons_remove {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : l ⊆ a :: (fun (x : α) => remove x l) a

theorem PointwiseComposition.List.remove_subset_remove {α : Type u_1} [DecidableEq α] (a : α) {l₁ l₂ : List α} (h : l₁ ⊆ l₂) : (fun (x : α) => remove x l₁) a ⊆ (fun (x : α) => remove x l₂) a

theorem PointwiseComposition.List.remove_cons_subset_cons_remove {α : Type u_1} [DecidableEq α] (a b : α) (l : List α) : (fun (x : α) => remove x (a :: l)) b ⊆ a :: (fun (x : α) => remove x l) b

theorem PointwiseComposition.List.remove_map_subset_map_remove {α : Type u_2} {β : Type u_1} [DecidableEq α] [DecidableEq β] (f : α → β) (l : List α) (a : α) : (fun (x : β) => remove x (List.map f l)) (f a) ⊆ List.map f ((fun (x : α) => remove x l) a)

theorem PointwiseComposition.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

def PointwiseComposition.List.inductionWithSingleton' {α : Type u_2} {motive : List α → Sort u_1} (hnil : motive []) (hsingle : (a : α) → motive [a]) (hcons : (a b : α) → (as : List α) → motive (b :: as) → motive (a :: b :: as)) (as : List α) : motive as

The induction with singleton' construction in List.

Equations

• PointwiseComposition.List.inductionWithSingleton' hnil hsingle hcons [] = hnil
• PointwiseComposition.List.inductionWithSingleton' hnil hsingle hcons [a] = hsingle a
• PointwiseComposition.List.inductionWithSingleton' hnil hsingle hcons (a :: b :: as) = hcons a b as (PointwiseComposition.List.inductionWithSingleton' hnil hsingle hcons (b :: as))

instance PointwiseComposition.List.Nodup.finite {α : Type u_1} [Finite α] : Finite { l : List α // l.Nodup }

theorem PointwiseComposition.List.suffix_of_cons_suffix {α : Type u_1} {l₁ l₂ : List α} {a : α} : a :: l₁ <:+ l₂ → l₁ <:+ l₂

theorem PointwiseComposition.List.suffix_cons_of {α : Type u_1} {l₁ l₂ : List α} {a : α} : l₁ <:+ l₂ → l₁ <:+ a :: l₂

theorem PointwiseComposition.List.exists_of_not_suffix {α : Type u_1} (l₁ l₂ : List α) : ¬l₁ <:+ l₂ → ∃ (l : List α) (a : α), a :: l <:+ l₁ ∧ l <:+ l₂ ∧ ¬a :: l <:+ l₂

theorem PointwiseComposition.List.IsSuffix.eq_or_cons_suffix {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+ l₂ → l₁ = l₂ ∨ ∃ (a : α✝), a :: l₁ <:+ l₂

theorem PointwiseComposition.List.suffix_trichotomy {α : Type u_1} {l₁ l₂ : List α} (h₁₂ : ¬l₁ <:+ l₂) (h₂₁ : ¬l₂ <:+ l₁) : ∃ (l : List α) (a : α) (b : α), a ≠ b ∧ a :: l <:+ l₁ ∧ b :: l <:+ l₂

theorem PointwiseComposition.List.Vector.get_mk_eq_get {α : Type u_1} {n : ℕ} (l : List α) (h : l.length = n) (i : Fin n) : List.Vector.get ⟨l, h⟩ i = l.get (Fin.cast ⋯ i)

theorem PointwiseComposition.List.Vector.get_one {α : Type u_2} {n : ℕ} (v : List.Vector α (n + 2)) : v.get 1 = v.tail.head

theorem PointwiseComposition.List.Vector.ofFn_vecCons {α : Type u_1} {n : ℕ} (a : α) (v : Fin n → α) : List.Vector.ofFn (a :> v) = a ::ᵥ List.Vector.ofFn v

theorem PointwiseComposition.List.Vector.cons_get {α : Type u_1} {k : ℕ} (a : α) (v : List.Vector α k) : (a ::ᵥ v).get = a :> v.get

theorem PointwiseComposition.List.exists_of_not_nil {α : Type u_1} {l : List α} (hl : l ≠ []) : ∃ (a : α), a ∈ l

theorem PointwiseComposition.List.iff_nil_forall {α : Type u_1} {l : List α} : l = [] ↔ ∀ a ∈ l, a ∈ []

theorem PointwiseComposition.List.nodup_iff_get_ne_get {α : Type u_1} {l : List α} : l.Nodup ↔ ∀ (i j : Fin l.length), i < j → l[i] ≠ l[j]

getElem version of List.nodup_iff_getElem?_ne_getElem?

theorem PointwiseComposition.List.Nodup.infinite_of_infinite {α : Type u_1} : Infinite { l : List α // l.Nodup } → Infinite α

theorem PointwiseComposition.List.exists_of_range {α✝ : Type u_1} {f : ℕ → α✝} {n : ℕ} {a : α✝} (h : a ∈ List.map f (List.range n)) : ∃ i < n, a = f i

theorem PointwiseComposition.List.single_suffix_uniq {α : Type u_1} {a b : α} {l : List α} (ha : [a] <:+ l) (hb : [b] <:+ l) : a = b