mono

Mathlib.Order.Directed

URI: https://scilib.ai/kg/mathlib#DirectedOn.mono

English

If s is DirectedOn r s and r a b implies r' a b for all a,b ∈ α, then DirectedOn r' s.

Русский

Если s направлено относительно r, и r a b ⇒ r' a b, тогда DirectedOn r' s.

LaTeX

$$$DirectedOn\\ r\\ s \\to (\\\\forall {a} {b}, r a b \\to r' a b) \\to DirectedOn\\ r'\\ s$$$

Lean4

theorem mono {s : Set α} (h : DirectedOn r s) (H : ∀ ⦃a b⦄, r a b → r' a b) : DirectedOn r' s :=
  h.mono' fun _ _ _ _ h ↦ H h

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

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

Разделы

Аффилиация

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