map_inj

Mathlib.Data.Option.Basic

URI: https://scilib.ai/kg/mathlib#Option.map_inj

English

Option.map is injective with respect to its two function arguments, i.e., map f = map g iff f = g.

Русский

Option.map инъективна по отношению к функциям f и g: map f = map g тогда и только тогда, когда f = g.

LaTeX

$$$$ \operatorname{map} f = \operatorname{map} g \iff f = g. $$$$

Lean4

@[simp]
theorem map_inj {f g : α → β} : Option.map f = Option.map g ↔ f = g :=
  map_injective'.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru