image_subset_diffs_left

Mathlib.Data.Finset.Sups

URI: https://scilib.ai/kg/mathlib#Finset.image_subset_diffs_left

English

If b ∈ t, then s.image (· \\ b) ⊆ s \\\\ t.

Русский

Если b ∈ t, то образ s по функции x ↦ x \\ b подпадает в s \\ t.

LaTeX

$$$ b \\in t \\to s.image (\\cdot \\setminus b) \\subseteq s \\\\ t $$$

Lean4

theorem image_subset_diffs_left : b ∈ t → s.image (· \ b) ⊆ s \\ t :=
  image_subset_image₂_left

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

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

Разделы

Аффилиация

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