image_val_mono

Mathlib.Data.Set.Subset

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

English

If D ⊆ E then the image satisfies ↑D ⊆ ↑E.

Русский

Если D ⊆ E, то образ ↑D ⊆ ↑E.

LaTeX

$$$ D \subseteq E \Rightarrow \uparrow D \subseteq \uparrow E $$$

Lean4

@[mono]
theorem image_val_mono (h : D ⊆ E) : (↑D : Set α) ⊆ ↑E :=
  (image_subset_image_iff Subtype.val_injective).2 h

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

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

Разделы

Аффилиация

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