prod_apply — Mathlib

English

There is a bijection between the product of quotients Quotient r × Quotient s and the quotient by the product Setoid r.prod s.

Русский

Существует биекция между произведением частичных факторов Quotient r × Quotient s и частотой Quotient (r.prod s).

LaTeX

$$$ (\operatorname{Quotient} r) \times (\operatorname{Quotient} s) \simeq \operatorname{Quotient}(r \mathrm{.prod} s) $$$

Lean4

theorem prod_apply {r : Setoid α} {s : Setoid β} {x₁ x₂ : α} {y₁ y₂ : β} :
    @Setoid.r _ (r.prod s) (x₁, y₁) (x₂, y₂) ↔ (@Setoid.r _ r x₁ x₂ ∧ @Setoid.r _ s y₁ y₂) :=
  Iff.rfl

Похожие утверждения