subtypeOrLeftEmbedding_apply — Mathlib

English

In general, subtypeOrLeftEmbedding p q x equals if p x then Sum.inl ⟨x, hx⟩ else Sum.inr ⟨x, x.prop.resolve_left hx⟩.

Русский

В общем случае subtypeOrLeftEmbedding p q x равна if p x then Sum.inl ⟨x, hx⟩ else Sum.inr ⟨x, x.prop.resolve_left hx⟩.

LaTeX

$$$\\text{subtypeOrLeftEmbedding } p q x = \\text{if } h: p x \\text{ then } \\mathrm{Sum.inl} \\langle x, h \\rangle \\text{ else } \\mathrm{Sum.inr} \\langle x, x.prop.resolve_left h \\rangle$$$

Lean4

@[grind =]
theorem subtypeOrLeftEmbedding_apply {p q : α → Prop} [DecidablePred p] (x : { x // p x ∨ q x }) :
    subtypeOrLeftEmbedding p q x = if h : p x then Sum.inl ⟨x, h⟩ else Sum.inr ⟨x, x.prop.resolve_left h⟩ :=
  rfl

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