image_val_inter_self_right_eq_coe

Mathlib.Data.Set.Subset

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

English

Let A ⊆ α and D ⊆ A. Then A ∩ ↑D = ↑D, i.e., the image of D is contained in A.

Русский

Пусть A ⊆ α и D ⊆ A. Тогда A ∩ ↑D = ↑D, то есть образ D содержится в A.

LaTeX

$$$ A \cap \uparrow D = \uparrow D $$$

Lean4

@[simp]
theorem image_val_inter_self_right_eq_coe : A ∩ ↑D = ↑D :=
  inter_eq_right.2 image_val_subset

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

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

Разделы

Аффилиация

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