subset_of_image_val_subset_image_val

Mathlib.Data.Set.Subset

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

English

If the image of D is contained in the image of E, then D ⊆ E.

Русский

Если образ D содержится в образе E, то D ⊆ E.

LaTeX

$$$ (\uparrow D \subseteq \uparrow E) \Rightarrow D \subseteq E $$$

Lean4

theorem subset_of_image_val_subset_image_val (h : (↑D : Set α) ⊆ ↑E) : D ⊆ E :=
  (image_subset_image_iff Subtype.val_injective).1 h

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

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

Разделы

Аффилиация

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