inter_right'

Mathlib.Data.Set.Disjoint

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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