extendSubtype_apply_of_mem — Mathlib

English

If x satisfies p, then extendSubtype x equals e applied to the corresponding subtype element.

Русский

Если x удовлетворяет условию p, то extendSubtype x равняется e примененному к соответствующему элементу подтипа.

LaTeX

$$$\text{extendSubtype}(e)(x) = e(\langle x, hx\rangle)$ при hx: p x$$

Lean4

theorem extendSubtype_apply_of_mem (e : { x // p x } ≃ { x // q x }) (x) (hx : p x) : e.extendSubtype x = e ⟨x, hx⟩ :=
  by
  dsimp only [extendSubtype]
  simp only [subtypeCongr, Equiv.trans_apply, Equiv.sumCongr_apply]
  rw [sumCompl_apply_symm_of_pos _ _ hx, Sum.map_inl, sumCompl_apply_inl]

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