bihimp_triangle

Mathlib.Order.SymmDiff

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

English

A triangle-type inequality for bihimp: min(bihimp(a,b), bihimp(b,c)) ≤ bihimp(a,c).

Русский

Неравенство типа треугольника для bihimp: min(bihimp(a,b), bihimp(b,c)) ≤ bihimp(a,c).

LaTeX

$$$\min\{ \operatorname{bihimp}(a,b), \operatorname{bihimp}(b,c) \} \le \operatorname{bihimp}(a,c)$$$

Lean4

theorem bihimp_triangle : a ⇔ b ⊓ b ⇔ c ≤ a ⇔ c :=
  @symmDiff_triangle αᵒᵈ _ _ _ _

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

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

Разделы

Аффилиация

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