English
There exists an equivalence between the subtype {x | p₂ x} and the quotient Quotient s₂, defined under hp₂ and h, i.e., {x | p₂ x} ≃ Quotient s₂.
Русский
Существует эквиваленция между подтипом {x | p₂ x} и частотой Quotient s₂, определяемая условиями hp₂ и h, то есть {x | p₂ x} ≃ Quotient s₂.
LaTeX
$$$\\{ x \\mid p₂ x \\} \\simeq \\operatorname{Quotient}(s₂)$$$
Lean4
/-- Subtype of the quotient is equivalent to the quotient of the subtype. Let `α` be a setoid with
equivalence relation `~`. Let `p₂` be a predicate on the quotient type `α/~`, and `p₁` be the lift
of this predicate to `α`: `p₁ a ↔ p₂ ⟦a⟧`. Let `~₂` be the restriction of `~` to `{x // p₁ x}`.
Then `{x // p₂ x}` is equivalent to the quotient of `{x // p₁ x}` by `~₂`. -/
def subtypeQuotientEquivQuotientSubtype (p₁ : α → Prop) {s₁ : Setoid α} {s₂ : Setoid (Subtype p₁)}
(p₂ : Quotient s₁ → Prop) (hp₂ : ∀ a, p₁ a ↔ p₂ ⟦a⟧) (h : ∀ x y : Subtype p₁, s₂.r x y ↔ s₁.r x y) :
{ x // p₂ x } ≃ Quotient s₂
where
toFun
a :=
Quotient.hrecOn a.1 (fun a h => ⟦⟨a, (hp₂ _).2 h⟩⟧)
(fun a b hab => hfunext (by rw [Quotient.sound hab]) fun _ _ _ => heq_of_eq (Quotient.sound ((h _ _).2 hab))) a.2
invFun
a :=
Quotient.liftOn a (fun a => (⟨⟦a.1⟧, (hp₂ _).1 a.2⟩ : { x // p₂ x })) fun _ _ hab =>
Subtype.ext (Quotient.sound ((h _ _).1 hab))
left_inv := by exact fun ⟨a, ha⟩ => Quotient.inductionOn a (fun b hb => rfl) ha
right_inv a := by exact Quotient.inductionOn a fun ⟨a, ha⟩ => rfl
