image_subset_image_iff

Mathlib.Data.Finset.Image

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

← MathLib Explorer

English

If f is injective, then s.image f ⊆ t.image f iff s ⊆ t.

Русский

Если f инъективна, то s.image f ⊆ t.image f тогда и только тогда, когда s ⊆ t.

LaTeX

$$$\text{Injective } f \Rightarrow (s.image f \subseteq t.image f) \iff (s \subseteq t)$$$

Lean4

theorem image_subset_image_iff {t : Finset α} (hf : Injective f) : s.image f ⊆ t.image f ↔ s ⊆ t :=
  mod_cast Set.image_subset_image_iff hf (s := s) (t := t)

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

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

Разделы

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

Аффилиация

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