inter_right

Mathlib.Data.Set.Disjoint

URI: https://scilib.ai/kg/mathlib#Disjoint.inter_right

English

If s is disjoint from t, then s is disjoint from (t ∩ u).

Русский

Если s несовместимо с t, то s несовместимо с (t ∩ u).

LaTeX

$$$Disjoint(s, (t \cap u)) \iff Disjoint(s,t)$$$

Lean4

theorem inter_right (u : Set α) (h : Disjoint s t) : Disjoint s (t ∩ u) :=
  h.inf_right _

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

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

Разделы

Аффилиация

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