image_subset_image_iff

Mathlib.Data.Set.Image

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

English

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

Русский

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

LaTeX

$$$f[S] \\subseteq f[T] \\iff S \\subseteq T \\quad \\text{for } f \\text{ injective}$$$

Lean4

theorem image_subset_image_iff {f : α → β} (hf : Injective f) : f '' s ⊆ f '' t ↔ s ⊆ t := by
  grind [Set.image_subset_iff, Set.preimage_image_eq]

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

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

Разделы

Аффилиация

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