rel_act_of_rel_of_rel_act

Mathlib.Algebra.Order.Monoid.Unbundled.Defs

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

English

For all m ∈ M and a,b,c ∈ N, if a ≤ b and c ≤ μ(m,a), then c ≤ μ(m,b).

Русский

Для всякого m и элементов a,b,c ∈ N, если a ≤ b и c ≤ μ(m,a), то c ≤ μ(m,b).

LaTeX

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

Lean4

theorem rel_act_of_rel_of_rel_act (ab : r a b) (rr : r c (μ m a)) : r c (μ m b) :=
  _root_.trans rr (act_rel_act_of_rel _ ab)

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

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

Разделы

Аффилиация

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