English
A subtype defined by p x ∨ q x embeds injectively into the sum of the subtypes {p x} ⊕ {q x}, sending elements with p to the left and those with ¬p to the right.
Русский
Подтип, заданный p x ∨ q x, инъективно встраивается в сумму подтипов {p x} ⊕ {q x}, отправляя элементы с p в левую часть, а элементы с ¬p — вправо.
LaTeX
$$$\\{ x \\mid p x \\lor q x \\} \\hookrightarrow (\\{ x \\mid p x \\} \\oplus \\{ x \\mid q x \\})$$$
Lean4
/-- A subtype `{x // p x ∨ q x}` over a disjunction of `p q : α → Prop` can be injectively split
into a sum of subtypes `{x // p x} ⊕ {x // q x}` such that `¬ p x` is sent to the right. -/
def subtypeOrLeftEmbedding (p q : α → Prop) [DecidablePred p] : { x // p x ∨ q x } ↪ { x // p x } ⊕ { x // q x } :=
⟨fun x => if h : p x then Sum.inl ⟨x, h⟩ else Sum.inr ⟨x, x.prop.resolve_left h⟩,
by
intro x y
dsimp only
split_ifs <;> simp [Subtype.ext_iff]⟩
