extendSubtype_apply_of_not_mem — Mathlib

English

Let e be an equivalence between the p-subtype and the q-subtype of a finite type α. For any x with ¬p x, the value of e.extendSubtype at x equals e.toCompl ⟨x, hx⟩.

Русский

Пусть e — эквивалент между подтипами {x | p x} и {x | q x} над конечным множество α. Для любого x с ¬p x выполнено e.extendSubtype x = e.toCompl ⟨x, hx⟩.

LaTeX

$$$ e.\\text{extendSubtype}(x) = e.\\text{toCompl}(\\langle x, \\neg p(x) \\rangle). $$$

Lean4

theorem extendSubtype_apply_of_not_mem (e : { x // p x } ≃ { x // q x }) (x) (hx : ¬p x) :
    e.extendSubtype x = e.toCompl ⟨x, hx⟩ := by
  dsimp only [extendSubtype]
  simp only [subtypeCongr, Equiv.trans_apply, Equiv.sumCongr_apply]
  rw [sumCompl_apply_symm_of_neg _ _ hx, Sum.map_inr, sumCompl_apply_inr]

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