sdiff_mem_diffs

Mathlib.Data.Finset.Sups

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

English

For any a ∈ s and b ∈ t, a \\ b ∈ s \\\\ t.

Русский

Если a ∈ s и b ∈ t, то a \\ b ∈ s \\\\ t.

LaTeX

$$$ a \\in s \\to b \\in t \\to a \\setminus b \\in s \\\\ t $$$

Lean4

theorem sdiff_mem_diffs : a ∈ s → b ∈ t → a \ b ∈ s \\ t :=
  mem_image₂_of_mem

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

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

Разделы

Аффилиация

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