subtypeOrLeftEmbedding_apply_right

English

If ¬ p x, then subtypeOrLeftEmbedding p q x equals Sum.inr ⟨x, x.prop.resolve_left hx⟩.

Русский

Если ¬ p x, то subtypeOrLeftEmbedding p q x равно Sum.inr ⟨x, x.prop.resolve_left hx⟩.

LaTeX

$$$\\text{if } \\neg p x\\text{ then } \\text{subtypeOrLeftEmbedding } p q x = \\mathrm{Sum.inr}(\\langle x, x.prop.resolve_left hx \\rangle)$$$

Lean4

@[simp]
theorem subtypeOrLeftEmbedding_apply_right {p q : α → Prop} [DecidablePred p] (x : { x // p x ∨ q x }) (hx : ¬p x) :
    subtypeOrLeftEmbedding p q x = Sum.inr ⟨x, x.prop.resolve_left hx⟩ :=
  dif_neg hx

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