subtypePreimage_symm_apply_coe_pos

English

For any x on the ¬p-subtype, and any a with p(a), the inverse image under subtypePreimage maps a to x0 at a's witness inside p.

Русский

Для любого x на подтипе ¬p и любого a с p(a), обратное отображение под subtypePreimage отправляет a в x0 при св-ве существования доказательства p.

LaTeX

$$$$ ((subtypePreimage\ p\ x_0).symm\ x)(a) = x_0\\langle a, h\\rangle \\quad\\text{for all } a\\in α\\text{ with } p(a). $$$$

Lean4

theorem subtypePreimage_symm_apply_coe_pos (x : { a // ¬p a } → β) (a : α) (h : p a) :
    ((subtypePreimage p x₀).symm x : α → β) a = x₀ ⟨a, h⟩ :=
  dif_pos h

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