Supporting results for pointwise provable equality.

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

def PointwiseComposition.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) → β

The lift Vec construction in Quotient.

Equations

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

@[simp]

theorem PointwiseComposition.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 ![]

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

@[simp]

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

@[simp]

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