def Quotient.finLiftOn₂ {ι₁ : Type u_1} [Fintype ι₁] [DecidableEq ι₁] {ι₂ : Type u_2} [Fintype ι₂] [DecidableEq ι₂] {α : ι₁ → Sort u_3} {S₁ : (i : ι₁) → Setoid (α i)} {β : ι₂ → Sort u_4} {S₂ : (i : ι₂) → Setoid (β i)} {φ : Sort u_5} (q₁ : (i : ι₁) → Quotient (S₁ i)) (q₂ : (i : ι₂) → Quotient (S₂ i)) (f : ((i : ι₁) → α i) → ((i : ι₂) → β i) → φ) (c : ∀ (a₁ : (i : ι₁) → α i) (b₁ : (i : ι₂) → β i) (a₂ : (i : ι₁) → α i) (b₂ : (i : ι₂) → β i), (∀ (i : ι₁), a₁ i ≈ a₂ i) → (∀ (i : ι₂), b₁ i ≈ b₂ i) → f a₁ b₁ = f a₂ b₂) : φ

Lift a binary function from its finitely indexed types ∀ i : ι₁, α i, ∀ i : ι₂, β i to a binary function on quotients. This is analogous to the combination of Quotient.finLiftOn and Quotient.liftOn₂.

Equations

• Quotient.finLiftOn₂ q₁ q₂ f c = (Quotient.finChoice q₁).liftOn₂ (Quotient.finChoice q₂) f c

@[simp]

theorem Quotient.finLiftOn₂_mk {ι₁ : Type u_1} [Fintype ι₁] [DecidableEq ι₁] {ι₂ : Type u_2} [Fintype ι₂] [DecidableEq ι₂] {α : ι₁ → Sort u_3} {S₁ : (i : ι₁) → Setoid (α i)} {β : ι₂ → Sort u_4} {S₂ : (i : ι₂) → Setoid (β i)} {φ : Sort u_5} (f : ((i : ι₁) → α i) → ((i : ι₂) → β i) → φ) (c : ∀ (a₁ : (i : ι₁) → α i) (b₁ : (i : ι₂) → β i) (a₂ : (i : ι₁) → α i) (b₂ : (i : ι₂) → β i), (∀ (i : ι₁), a₁ i ≈ a₂ i) → (∀ (i : ι₂), b₁ i ≈ b₂ i) → f a₁ b₁ = f a₂ b₂) (a : (i : ι₁) → α i) (b : (i : ι₂) → β i) : finLiftOn₂ (fun (x : ι₁) => ⟦a x⟧) (fun (x : ι₂) => ⟦b x⟧) f c = f a b