optionElim — Mathlib

English

The underlying function of sumSet is the standard sum-elimination function Sum.elim.

Русский

Базовая функция sumSet равна обычной функции Sum.elim.

LaTeX

$$$\\text{coe}(\\text{sumSet } h) = \\text{Sum.elim } (\\uparrow) (\\uparrow)$$$

Lean4

/-- Given an embedding `f : α ↪ β` and a point outside of `Set.range f`, construct an embedding
`Option α ↪ β`. -/
@[simps]
def optionElim {α β} (f : α ↪ β) (x : β) (h : x ∉ Set.range f) : Option α ↪ β :=
  ⟨Option.elim' x f, Option.injective_iff.2 ⟨f.2, h⟩⟩

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