mem_map_of_injective

Mathlib.Data.Option.Basic

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

← MathLib Explorer

English

If f is injective, then f a ∈ o.map f iff a ∈ o.

Русский

Если f инъективна, то f a ∈ o.map f эквивалентно a ∈ o.

LaTeX

$$$$ \forall {f} (H : Function.Injective f) {a} {o}, f \; a \in o.map f \iff a \in o. $$$$

Lean4

@[simp 1100, nolint simpNF]
theorem mem_map_of_injective {f : α → β} (H : Function.Injective f) {a : α} {o : Option α} : f a ∈ o.map f ↔ a ∈ o := by
  aesop

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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