extendSubtype_not_mem — Mathlib

English

Let e be as above. If p x is false, then e.extendSubtype x does not lie in q-subtype, i.e., ¬ q (e.extendSubtype x).

Русский

Пусть e — как выше. Если p x ложно, то e.extendSubtype x не принадлежит подтипy q, то есть ¬ q (e.extendSubtype x).

LaTeX

$$$ \\neg q (e.extendSubtype x) $$$

Lean4

theorem extendSubtype_not_mem (e : { x // p x } ≃ { x // q x }) (x) (hx : ¬p x) : ¬q (e.extendSubtype x) :=
  by
  convert (e.toCompl ⟨x, hx⟩).2
  rw [e.extendSubtype_apply_of_not_mem _ hx]

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