sup_inf_bihimp

Mathlib.Order.SymmDiff

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

English

A core identity states that min(bihimp(a,b), a ∨ b) = a ∧ b.

Русский

Основная тождественность: min( bihimp(a,b), a ∨ b ) = a ∧ b.

LaTeX

$$$\min\big( \operatorname{bihimp}(a,b), a \lor b \big) = a \land b$$$

Lean4

@[simp]
theorem sup_inf_bihimp : (a ⊔ b) ⊓ a ⇔ b = a ⊓ b :=
  @inf_sup_symmDiff αᵒᵈ _ _ _

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

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

Разделы

Аффилиация

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