English
For a setoid α, given g: Quotient α → β and h: α → β with Hh: h = g ∘ Quotient.mk'', and r ⊆ β×β, the specified equality of sets holds between a preimage under h and an image under a map sending a pair to their quotient representatives.
Русский
Для множества равенств α, дано g: Quotient α → β и h: α → β с Hh: h = g ∘ Quotient.mk'', и r ⊆ β×β; выполняется заданное равенство множеств между предварительным образованием по h и образом по отображению, отправляющему пару на их представителя в факторе.
LaTeX
$$$\\{x : \\Quotient s \\times \\Quotient s \\mid (g\,x.1, g\,x.2) \\in r\\} = \\left( a \\mapsto (\\overline{a_1}, \\overline{a_2}) \\right) '' ((a_1,a_2) \\mapsto (h a_1, h a_2))^{-1} r$$$
Lean4
theorem prod_quotient_preimage_eq_image [s : Setoid α] (g : Quotient s → β) {h : α → β} (Hh : h = g ∘ Quotient.mk'')
(r : Set (β × β)) :
{x : Quotient s × Quotient s | (g x.1, g x.2) ∈ r} =
(fun a : α × α => (⟦a.1⟧, ⟦a.2⟧)) '' ((fun a : α × α => (h a.1, h a.2)) ⁻¹' r) :=
Hh.symm ▸
Set.ext fun ⟨a₁, a₂⟩ =>
⟨Quot.induction_on₂ a₁ a₂ fun a₁ a₂ h => ⟨(a₁, a₂), h, rfl⟩, fun ⟨⟨b₁, b₂⟩, h₁, h₂⟩ =>
show (g a₁, g a₂) ∈ r from
have h₃ : ⟦b₁⟧ = a₁ ∧ ⟦b₂⟧ = a₂ := Prod.ext_iff.1 h₂
h₃.1 ▸ h₃.2 ▸ h₁⟩
