subtypeOrLeftEmbedding_apply_left

English

If x is in the left branch (p x), then subtypeOrLeftEmbedding p q x equals Sum.inl ⟨x, hx⟩.

Русский

Если x лежит в левой ветви (p x), то subtypeOrLeftEmbedding p q x равняется Sum.inl ⟨x, hx⟩.

LaTeX

$$$\\text{if } hx: p x\\text{ then } \\text{subtypeOrLeftEmbedding } p q x = \\mathrm{Sum.inl}(\\langle x, hx \\rangle)$$$

Lean4

@[simp]
theorem subtypeOrLeftEmbedding_apply_left {p q : α → Prop} [DecidablePred p] (x : { x // p x ∨ q x }) (hx : p x) :
    subtypeOrLeftEmbedding p q x = Sum.inl ⟨x, hx⟩ :=
  dif_pos hx

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