inf_left

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Codisjoint.inf_left

English

Given ha: Codisjoint a c and hb: Codisjoint b c, then Codisjoint (a ∧ b) c.

Русский

Если ha: Codisjoint a c и hb: Codisjoint b c, тогда Codisjoint (a ∧ b) c.

LaTeX

$$$Codisjoint a c \rightarrow Codisjoint b c \rightarrow Codisjoint (a \wedge b) c$$$

Lean4

theorem inf_left (ha : Codisjoint a c) (hb : Codisjoint b c) : Codisjoint (a ⊓ b) c :=
  codisjoint_inf_left.2 ⟨ha, hb⟩

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

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

Разделы

Аффилиация

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