image_eq_image

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.image_eq_image

← MathLib Explorer

English

If f is injective, then f[S] = f[T] ⇔ S = T.

Русский

Если f инъективна, то f[S] = f[T] ⇔ S = T.

LaTeX

$$$f''s = f''t \\iff s = t \\quad \\text{assuming } \\text{Injective}(f)$$$

Lean4

theorem image_eq_image {f : α → β} (hf : Injective f) : f '' s = f '' t ↔ s = t :=
  Iff.symm <| (Iff.intro fun eq => eq ▸ rfl) fun eq => by rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, eq]

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

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

Разделы

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

Аффилиация

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