rel_of_act_rel_act

Mathlib.Algebra.Order.Monoid.Unbundled.Defs

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

English

If μ(m,a) ≤ μ(m,b), then a ≤ b.

Русский

Если μ(m,a) ≤ μ(m,b), то a ≤ b.

LaTeX

$$$\forall m\in M\;\forall a,b\in N,\ r(\mu\,m\,a,\mu\,m\,b) \to r(a,b)$$$

Lean4

theorem rel_of_act_rel_act (m : M) {a b : N} (ab : r (μ m a) (μ m b)) : r a b :=
  ContravariantClass.elim _ ab

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

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

Разделы

Аффилиация

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