inter_left

Mathlib.Data.Set.Disjoint

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

English

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

Русский

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

LaTeX

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

Lean4

theorem inter_left (u : Set α) (h : Disjoint s t) : Disjoint (s ∩ u) t :=
  h.inf_left _

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

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

Разделы

Аффилиация

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