map_injective' — Mathlib

English

The map from functions to functions, f ↦ Option.map f, is injective.

Русский

Отображение функций в функции, f ↦ Option.map f, инъективно.

LaTeX

$$$$ \forall f g, \mathrm{Option.map} f = \mathrm{Option.map} g \Rightarrow f = g. $$$$

Lean4

/-- `Option.map` as a function between functions is injective. -/
theorem map_injective' : Function.Injective (@Option.map α β) := fun f g h ↦
  funext fun x ↦ some_injective _ <| by simp only [← map_some, h]

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