sup_mem_sups

Mathlib.Data.Finset.Sups

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

English

If s1 ⊆ s2 and t1 ⊆ t2 then s1 ⊻ t1 ⊆ s2 ⊻ t2.

Русский

Если s1 ⊆ s2 и t1 ⊆ t2, то s1 ⊻ t1 ⊆ s2 ⊻ t2.

LaTeX

$$$ s_1 \\subseteq s_2 \\to t_1 \\subseteq t_2 \\to s_1 \\oplus t_1 \\subseteq s_2 \\oplus t_2 $$$

Lean4

theorem sup_mem_sups : a ∈ s → b ∈ t → a ⊔ b ∈ s ⊻ t :=
  mem_image₂_of_mem

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

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

Разделы

Аффилиация

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