mem_set_image

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Function.Injective.mem_set_image

← MathLib Explorer

English

If f is injective, then f(a) ∈ f''s if and only if a ∈ s.

Русский

Если f инъективна, то f(a) ∈ f''s тогда и только тогда, когда a ∈ s.

LaTeX

$$$ f(a) \\in f''s \\iff a \\in s. $$$

Lean4

theorem _root_.Function.Injective.mem_set_image {f : α → β} (hf : Injective f) {s : Set α} {a : α} :
    f a ∈ f '' s ↔ a ∈ s :=
  ⟨fun ⟨_, hb, Eq⟩ => hf Eq ▸ hb, by grind⟩

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

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

Разделы

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

Аффилиация

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