isDirected_mono

Mathlib.Order.Directed

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

← MathLib Explorer

English

If IsDirected α r and r a b implies s a b, then IsDirected α s.

Русский

Если IsDirected α r и r a b ⇒ s a b, то IsDirected α s.

LaTeX

$$[IsDirected α r] \\to (\\\\forall {a b}, r a b \\\\to s a b) \\\\Rightarrow IsDirected α s$$

Lean4

theorem isDirected_mono [IsDirected α r] (h : ∀ ⦃a b⦄, r a b → s a b) : IsDirected α s :=
  ⟨fun a b =>
    let ⟨c, ha, hb⟩ := IsDirected.directed a b
    ⟨c, h ha, h hb⟩⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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