sup_eq_left

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.sup_eq_left

English

If b ≤ a, then a ⊔ b is equivalent to a under the CauSeq equivalence.

Русский

Если b ≤ a, то a ⊔ b эквивалентно a.

LaTeX

$$$\forall a,b\in \mathrm{CauSeq}(\alpha, \mathrm{abs})\; (b \le a) \Rightarrow (a \vee b) \approx a$$$

Lean4

protected theorem sup_eq_left {a b : CauSeq α abs} (h : b ≤ a) : a ⊔ b ≈ a := by
  simpa only [CauSeq.sup_comm] using CauSeq.sup_eq_right h

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

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

Разделы

Аффилиация

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