inf_right

Mathlib.Order.Disjoint

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

English

If hb: Codisjoint a b and hc: Codisjoint a c, then Codisjoint a (b ∧ c).

Русский

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

LaTeX

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

Lean4

theorem inf_right (hb : Codisjoint a b) (hc : Codisjoint a c) : Codisjoint a (b ⊓ c) :=
  codisjoint_inf_right.2 ⟨hb, hc⟩

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

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

Разделы

Аффилиация

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