inf_sdiff_distrib_right

Mathlib.Order.BooleanAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#inf_sdiff_distrib_right

English

a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c).

Русский

a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c).

LaTeX

$$$$ a \setminus b \land c = (a \land c) \setminus (b \land c) $$$$

Lean4

theorem inf_sdiff_distrib_right (a b c : α) : a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c) := by
  simp_rw [inf_comm _ c, inf_sdiff_distrib_left]

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

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

Разделы

Аффилиация

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