coe_subtypeEquiv_eq_map — Mathlib

English

The underlying function of subtypeEquiv equals Subtype.map composed with the given equivalence on the base types.

Русский

Функция-основание subtypeEquiv равна Subtype.map композицией с данным тождественным соответствием между базовыми типами.

LaTeX

$$$$ \\text{toFun}(e.subtypeEquiv h) = \\text{Subtype.map}(e, h \\cdot |>.mp). $$$$

Lean4

theorem coe_subtypeEquiv_eq_map {X Y} {p : X → Prop} {q : Y → Prop} (e : X ≃ Y) (h : ∀ x, p x ↔ q (e x)) :
    ⇑(e.subtypeEquiv h) = Subtype.map e (h · |>.mp) :=
  rfl

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