image_val_preimage_val_subset_self

Mathlib.Data.Set.Subset

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

English

The image of A ∩ B under inclusion is contained in B: ↑(A ↓∩ B) ⊆ B.

Русский

Образ A ↓∩ B под включением содержится в B: ↑(A ↓∩ B) ⊆ B.

LaTeX

$$$ \uparrow (A \downarrow\cap B) \subseteq B $$$

Lean4

theorem image_val_preimage_val_subset_self : ↑(A ↓∩ B) ⊆ B :=
  image_preimage_subset _ _

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

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

Разделы

Аффилиация

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