English
Let p₁ be a predicate on α, with s₁ a Setoid on α and s₂ a Setoid on Subtype p₁. Then the equivalence subtypeQuotientEquivQuotientSubtype(p₁,p₂, hp₂, h) maps a pair ⟨⎯⟦x⎧, hx⟩ to an element of Quotient s₂ in a canonical way, i.e., the forward map respects the quotient structure defined by s₂.
Русский
Пусть p₁ — предикат на α, s₁ — множество эквивалентности на α, s₂ — множество эквивалентности на подпредикат p₁. Тогда отображение subtypeQuotientEquivQuotientSubtype(p₁,p₂, hp₂, h) переводит элемент ⟨⟦x⟧, hx⟩ в элемент Quotient s₂ канонически, сохраняя структуру эквиваленций.
LaTeX
$$$\\text{equiv} : { x \\mid p₂ x } \\to \\operatorname{Quotient}(s₂)$, $\\text{forward} \\; (x,h) \\mapsto \\operatorname{Quotient.mk}(s₂, x)$, $\\text{reverse} \\; [q] \\mapsto \\text{representative}$$$
Lean4
theorem subtypeEquivCodomain_symm_apply_ne (f : { x' // x' ≠ x } → Y) (y : Y) (x' : X) (h : x' ≠ x) :
((subtypeEquivCodomain f).symm y : X → Y) x' = f ⟨x', h⟩ :=
dif_pos h
