image_subset_sups_left

Mathlib.Data.Set.Sups

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

English

For b ∈ t, the image (a ↦ a ⊔ b) of s is contained in s ⊻ t.

Русский

Для b ∈ t образ множества s под отображением a ↦ a ⊔ b содержится в s ⊻ t.

LaTeX

$$$ b \in t \Rightarrow ( \{ a \uplus b \mid a \in s \} \subseteq s \ ⊻ \ t )$$$

Lean4

theorem image_subset_sups_left : b ∈ t → (fun a => a ⊔ b) '' s ⊆ s ⊻ t :=
  image_subset_image2_left

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

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

Разделы

Аффилиация

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