surjective_restrict — Mathlib

English

Restriction map f ↦ restrict p f is surjective: every function on the restricted domain extends to a function on the whole domain.

Русский

Отображение ограничения f ↦ restrict p f сюръективно: любую функцию на ограниченной области можно продолжить до функции на всей области.

LaTeX

$$$\\mathrm{Surjective}\\; (\\lambda f, \\mathrm{restrict}\\ p\\ f)$$$

Lean4

theorem surjective_restrict {α} {β : α → Type*} [ne : ∀ a, Nonempty (β a)] (p : α → Prop) :
    Surjective fun f : ∀ x, β x ↦ restrict p f := by
  classical exact fun f ↦ ⟨fun x ↦ if h : p x then f ⟨x, h⟩ else Nonempty.some (ne x), by grind⟩

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