subtypePreimage_symm_apply_coe_neg

English

For x on the ¬p-subtype and a with ¬p(a), the inverse image under subtypePreimage maps a to x⟨a, h⟩.

Русский

Для x на подтипе ¬p и для a с ¬p(a) обратное отображение под subtypePreimage отправляет a в x⟨a, h⟩.

LaTeX

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

Lean4

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

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