mk_arrow — Mathlib

English

For any subobject P of X, the construction mk P.arrow returns P again.

Русский

Для любого подобъекта P ⊆ X конструирование mk P.arrow возвращает P.

LaTeX

$$$\\text{mk } P.arrow = P$$$

Lean4

@[simp]
theorem mk_arrow (P : Subobject X) : mk P.arrow = P :=
  Quotient.inductionOn' P fun Q =>
    by
    obtain ⟨e⟩ := @Quotient.mk_out' _ (isIsomorphicSetoid _) Q
    exact Quotient.sound' ⟨MonoOver.isoMk (Iso.refl _) ≪≫ e⟩

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