inf_eq_left

Mathlib.Algebra.Order.CauSeq.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

protected theorem inf_eq_left {a b : CauSeq α abs} (h : a ≤ b) : a ⊓ b ≈ a := by
  simpa only [CauSeq.inf_comm] using CauSeq.inf_eq_right h

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

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

Разделы

Аффилиация

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