disjoint_of_subset

Mathlib.Data.Set.Disjoint

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

English

If s1 ⊆ s2 and t1 ⊆ t2 and Disjoint s2 t2, then Disjoint s1 t1.

Русский

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

LaTeX

$$$s_1 \subseteq s_2 \to t_1 \subseteq t_2 \to \mathrm{Disjoint}(s_2,t_2) \to \mathrm{Disjoint}(s_1,t_1)$$$

Lean4

@[gcongr high]
theorem disjoint_of_subset (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) (h : Disjoint s₂ t₂) : Disjoint s₁ t₁ :=
  h.mono hs ht

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

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

Разделы

Аффилиация

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