inter_left'

Mathlib.Data.Set.Disjoint

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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